:: Abian's Fixed Point Theorem
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 22, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

definition
let i be Integer;
attri is even  means :Def1: :: ABIAN:def 1
2 divides i;
end;

:: deftheorem Def1 defines even ABIAN:def_1_:_
 for i being Integer holds
( i is even iff 2 divides i );

notation
let i be Integer;
antonym  odd i for  even ;
end;

Lm1:  for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j )
proofend;

definition
let n be Element of NAT ;
redefine attr n is even  means :: ABIAN:def 2
 ex k being Element of NAT st n = 2 * k;
compatibility
 ( n is even iff ex k being Element of NAT st n = 2 * k )
proofend;
end;

:: deftheorem  defines even ABIAN:def_2_:_
 for n being Element of NAT holds
( n is even iff ex k being Element of NAT st n = 2 * k );

registration
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() even for Element of NAT ;
existence
 ex b1 being Element of NAT st b1 is even
proofend;
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() odd for Element of NAT ;
existence
 ex b1 being Element of NAT st b1 is odd
proofend;
cluster ext-real complex V18() integer even for set ;
existence
 ex b1 being Integer st b1 is even
proofend;
cluster ext-real complex V18() integer odd for set ;
existence
 ex b1 being Integer st b1 is odd
proofend;
end;

theorem Th1: :: ABIAN:1
for i being Integer holds
( i is odd iff ex j being Integer st i = (2 * j) + 1 )
proofend;

registration
let i be Integer;
cluster2 * i ->  even ;
coherence
 2 * i is even by Lm1;
end;

registration
let i be even Integer;
clusteri + 1 ->  odd ;
coherence
 not i + 1 is even
proofend;
end;

registration
let i be odd Integer;
clusteri + 1 ->  even ;
coherence
 i + 1 is even
proofend;
end;

registration
let i be even Integer;
clusteri - 1 ->  odd ;
coherence
 not i - 1 is even
proofend;
end;

registration
let i be odd Integer;
clusteri - 1 ->  even ;
coherence
 i - 1 is even
proofend;
end;

registration
let i be even Integer;
let j be Integer;
clusteri * j ->  even ;
coherence
 i * j is even
proofend;
clusterj * i ->  even ;
coherence
 j * i is even ;
end;

registration
let i, j be odd Integer;
clusteri * j ->  odd ;
coherence
 not i * j is even
proofend;
end;

registration
let i, j be even Integer;
clusteri + j ->  even ;
coherence
 i + j is even
proofend;
end;

registration
let i be even Integer;
let j be odd Integer;
clusteri + j ->  odd ;
coherence
 not i + j is even
proofend;
clusterj + i ->  odd ;
coherence
 not j + i is even ;
end;

registration
let i, j be odd Integer;
clusteri + j ->  even ;
coherence
 i + j is even
proofend;
end;

registration
let i be even Integer;
let j be odd Integer;
clusteri - j ->  odd ;
coherence
 not i - j is even
proofend;
clusterj - i ->  odd ;
coherence
 not j - i is even
proofend;
end;

registration
let i, j be odd Integer;
clusteri - j ->  even ;
coherence
 i - j is even
proofend;
end;

registration
let m be even Integer;
clusterm + 2 ->  even ;
coherence
 m + 2 is even
proofend;
end;

registration
let m be odd Integer;
clusterm + 2 ->  odd ;
coherence
 not m + 2 is even
proofend;
end;

definition
let E be set ;
let f be Function of E,E;
let n be Element of NAT ;
:: original:iter
redefine func iter (f,n) ->  Function of E,E;
coherence
 iter (f,n) is Function of E,E by FUNCT_7:83;
end;

theorem Th2: :: ABIAN:2
for S being non empty Subset of NAT st 0 in S holds
min S = 0
proofend;

theorem Th3: :: ABIAN:3
for E being non empty set
for f being Function of E,E
for x being Element of E holds (iter (f,0)) . x = x
proofend;

:: from KNASTER, 2005.02.06, A.T.
definition
let x be set ;
let f be Function;
predx is_a_fixpoint_of f means :Def3: :: ABIAN:def 3
( x in dom f & x = f . x );
end;

:: deftheorem Def3 defines is_a_fixpoint_of ABIAN:def_3_:_
 for x being set
for f being Function holds
( x is_a_fixpoint_of f iff ( x in dom f & x = f . x ) );

definition
let A be non empty set ;
let a be Element of A;
let f be Function of A,A;
:: original:is_a_fixpoint_of
redefine preda is_a_fixpoint_of f means :Def4: :: ABIAN:def 4
a = f . a;
compatibility
 ( a is_a_fixpoint_of f iff a = f . a )
proofend;
end;

:: deftheorem Def4 defines is_a_fixpoint_of ABIAN:def_4_:_
 for A being non empty set
for a being Element of A
for f being Function of A,A holds
( a is_a_fixpoint_of f iff a = f . a );

definition
let f be Function;
attrf is with_fixpoint  means :Def5: :: ABIAN:def 5
 ex x being set st x is_a_fixpoint_of f;
end;

:: deftheorem Def5 defines with_fixpoint ABIAN:def_5_:_
 for f being Function holds
( f is with_fixpoint iff ex x being set st x is_a_fixpoint_of f );

notation
let f be Function;
antonym  without_fixpoints f for  with_fixpoint ;
end;

definition
let X be set ;
let x be Element of X;
attrx is covering  means :Def6: :: ABIAN:def 6
 union x = union (union X);
end;

:: deftheorem Def6 defines covering ABIAN:def_6_:_
 for X being set
for x being Element of X holds
( x is covering iff union x = union (union X) );

theorem Th4: :: ABIAN:4
for E being set
for sE being Subset-Family of E holds
( sE is covering iff union sE = E )
proofend;

registration
let E be set ;
cluster non empty finite covering for Element of bool (bool E);
existence
 ex b1 being Subset-Family of E st
( not b1 is empty & b1 is finite & b1 is covering )
proofend;
end;

theorem :: ABIAN:5
for E being set
for f being Function of E,E
for 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
proofend;

definition
let E be set ;
let f be Function of E,E;
func =_ f ->  Equivalence_Relation of E means :Def7: :: ABIAN:def 7
 for x, y being set st x in E & y in E holds
( [x,y] in it iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y );
existence
 ex b1 being Equivalence_Relation of E st
for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of E st ( for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) & ( for x, y being set st x in E & y in E holds
( [x,y] in b2 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines =_ ABIAN:def_7_:_
 for E being set
for f being Function of E,E
for b3 being Equivalence_Relation of E holds
( b3 = =_ f iff for x, y being set st x in E & y in E holds
( [x,y] in b3 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) );

theorem Th6: :: ABIAN:6
for E being non empty set
for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c holds f . e in c
proofend;

theorem Th7: :: ABIAN:7
for E being non empty set
for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter (f,n)) . e in c
proofend;

registration
cluster empty-membered  ->  trivial for set ;
coherence
 for b1 being set st b1 is empty-membered holds
b1 is trivial ;
end;

registration
let A be set ;
let B be with_non-empty_element set ;
cluster Relation-like non-empty A -defined B -valued Function-like V33(A,B) for Element of bool [:A,B:];
existence
 ex b1 being Function of A,B st b1 is non-empty
proofend;
end;

registration
let A be non empty set ;
let B be with_non-empty_element set ;
let f be non-empty Function of A,B;
let a be Element of A;
clusterf . a ->  non empty ;
coherence
 not f . a is empty
proofend;
end;

registration
let X be non empty set ;
cluster bool X ->  with_non-empty_element ;
coherence
 not bool X is empty-membered
proofend;
end;

theorem :: ABIAN:8
for E being non empty set
for f being Function of E,E st f is without_fixpoints holds
ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
proofend;

begin

:: from SCMFSA9A, 2006.03.14, A.T.
theorem :: ABIAN:9
for n being Nat holds
( n is odd iff ex k being Element of NAT st n = (2 * k) + 1 )
proofend;

:: missing, 2008.03.20, A.T.
theorem :: ABIAN:10
for n being Element of NAT
for A being non empty set
for f being Function of A,A
for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
proofend;

theorem :: ABIAN:11
for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j ) by Lm1;

:: from HEYTING3, MOEBIUS1, 2010.02.13, A.T.
registration
cluster ext-real V10() V11() V12() V16() complex V18() integer odd for set ;
existence
 ex b1 being Nat st b1 is odd
proofend;
cluster ext-real V10() V11() V12() V16() complex V18() integer even for set ;
existence
 ex b1 being Nat st b1 is even
proofend;
end;

theorem Th12: :: ABIAN:12
for n being odd Nat holds 1 <= n
proofend;

registration
cluster integer odd  ->  non zero for set ;
coherence
 for b1 being Integer st b1 is odd holds
not b1 is zero by Th12;
end;