:: Abian's Fixed Point Theorem :: by Piotr Rudnicki and Andrzej Trybulec :: :: Received February 22, 1997 :: Copyright (c) 1997-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SETFAM_1, FUNCT_1, SUBSET_1, INT_1, RELAT_1, CARD_1, XXREAL_0, ARYTM_3, ARYTM_1, FUNCT_7, XBOOLE_0, TARSKI, ZFMISC_1, FINSET_1, EQREL_1, FUNCOP_1, ABIAN, XCMPLX_0, NAT_1, RECDEF_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, MCART_1, DOMAIN_1, FINSET_1, SETFAM_1, SEQ_4, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, INT_1, NAT_1, NAT_D, EQREL_1, FUNCT_7, XXREAL_0; constructors SETFAM_1, XXREAL_0, REAL_1, NAT_1, NAT_D, EQREL_1, SEQ_4, REALSET1, FUNCT_7, XXREAL_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, XREAL_0, INT_1, MEMBERED, EQREL_1, XXREAL_2, XXREAL_0, NAT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x, y, z, E, E1, E2, E3 for set, sE for Subset-Family of E, f for Function of E, E, k, l, m, n for Nat; definition let i be Integer; attr i is even means :: ABIAN:def 1 2 divides i; end; notation let i be Integer; antonym i is odd for i is even; end; definition let n be Nat; redefine attr n is even means :: ABIAN:def 2 ex k st n = 2*k; end; registration cluster even for Nat; cluster odd for Nat; cluster even for Element of NAT; cluster odd for Element of NAT; cluster even for Integer; cluster odd for Integer; end; theorem :: ABIAN:1 for i being Integer holds i is odd iff ex j being Integer st i = 2*j+1; registration let i be Integer; cluster 2*i -> even; end; registration let i be even Integer; cluster i+1 -> odd; end; registration let i be odd Integer; cluster i+1 -> even; end; registration let i be even Integer; cluster i-1 -> odd; end; registration let i be odd Integer; cluster i-1 -> even; end; registration let i be even Integer, j be Integer; cluster i*j -> even; cluster j*i -> even; end; registration let i, j be odd Integer; cluster i*j -> odd; end; registration let i, j be even Integer; cluster i+j -> even; end; registration let i be even Integer, j be odd Integer; cluster i+j -> odd; cluster j+i -> odd; end; registration let i, j be odd Integer; cluster i+j -> even; end; registration let i be even Integer, j be odd Integer; cluster i-j -> odd; cluster j-i -> odd; end; registration let i, j be odd Integer; cluster i-j -> even; end; registration let m be even Integer; cluster m + 2 -> even; end; registration let m be odd Integer; cluster m + 2 -> odd; end; definition let E, f; let n be Nat; redefine func iter(f, n) -> Function of E, E; end; theorem :: ABIAN:2 for S being non empty Subset of NAT st 0 in S holds min S = 0; theorem :: ABIAN:3 for E being non empty set, f being Function of E, E, x being Element of E holds iter(f,0).x = x; :: from KNASTER, 2005.02.06, A.T. definition let x be object, f be Function; pred x is_a_fixpoint_of f means :: ABIAN:def 3 x in dom f & x = f.x; end; definition let A be non empty set, a be Element of A, f be Function of A, A; redefine pred a is_a_fixpoint_of f means :: ABIAN:def 4 a = f.a; end; definition let f be Function; attr f is with_fixpoint means :: ABIAN:def 5 ex x being object st x is_a_fixpoint_of f; end; notation let f be Function; antonym f is without_fixpoints for f is with_fixpoint; end; definition let X be set, x be Element of X; attr x is covering means :: ABIAN:def 6 union x = union union X; end; theorem :: ABIAN:4 sE is covering iff union sE = E; registration let E; cluster non empty finite covering for Subset-Family of E; end; theorem :: ABIAN:5 for E being set, f being Function of E, E, sE being non empty covering Subset-Family of E st for X being Element of sE holds X misses f.:X holds f is without_fixpoints; definition let E, f; func =_f -> Equivalence_Relation of E means :: ABIAN:def 7 for x, y st x in E & y in E holds [x,y] in it iff ex k, l st iter(f,k).x = iter(f,l).y; end; theorem :: ABIAN:6 for E being non empty set, f being Function of E, E, c being Element of Class =_f, e being Element of c holds f.e in c; theorem :: ABIAN:7 for E being non empty set, f being Function of E, E, c being Element of Class =_f, e being Element of c, n holds iter(f, n).e in c; registration cluster empty-membered -> trivial for set; end; registration let A be set, B be with_non-empty_element set; cluster non-empty for Function of A, B; end; registration let A be non empty set, B be with_non-empty_element set, f be non-empty Function of A, B, a be Element of A; cluster f.a -> non empty; end; registration let X be non empty set; cluster bool X -> with_non-empty_element; end; theorem :: ABIAN:8 for E being non empty set, f being Function of E, E st f is without_fixpoints ex E1, E2, E3 st E1 \/ E2 \/ E3 = E & f.:E1 misses E1 & f.:E2 misses E2 & f.:E3 misses E3; begin :: Addenda :: from SCMFSA9A, 2006.03.14, A.T. theorem :: ABIAN:9 for n being Nat holds n is odd iff ex k being Nat st n = 2*k+1; :: missing, 2008.03.20, A.T. theorem :: ABIAN:10 for A being non empty set, f being Function of A,A, x being Element of A holds iter(f,n+1).x = f.(iter(f,n).x); theorem :: ABIAN:11 for i being Integer holds i is even iff ex j being Integer st i = 2*j; :: from HEYTING3, MOEBIUS1, 2010.02.13, A.T. registration cluster odd for Nat; cluster even for Nat; end; theorem :: ABIAN:12 for n being odd Nat holds 1 <= n; registration cluster odd -> non zero for Integer; end;