:: 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;
attr i 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 )
proof end;

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 )
proof end;
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
proof end;
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
proof end;
cluster ext-real complex V18() integer even for set ;
existence
ex b1 being Integer st b1 is even
proof end;
cluster ext-real complex V18() integer odd for set ;
existence
ex b1 being Integer st b1 is odd
proof end;
end;

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

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

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

registration
let i be odd Integer;
cluster i + 1 -> even ;
coherence
i + 1 is even
proof end;
end;

registration
let i be even Integer;
cluster i - 1 -> odd ;
coherence
not i - 1 is even
proof end;
end;

registration
let i be odd Integer;
cluster i - 1 -> even ;
coherence
i - 1 is even
proof end;
end;

registration
let i be even Integer;
let j be Integer;
cluster i * j -> even ;
coherence
i * j is even
proof end;
cluster j * i -> even ;
coherence
j * i is even ;
end;

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

registration
let i, j be even Integer;
cluster i + j -> even ;
coherence
i + j is even
proof end;
end;

registration
let i be even Integer;
let j be odd Integer;
cluster i + j -> odd ;
coherence
not i + j is even
proof end;
cluster j + i -> odd ;
coherence
not j + i is even ;
end;

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

registration
let i be even Integer;
let j be odd Integer;
cluster i - j -> odd ;
coherence
not i - j is even
proof end;
cluster j - i -> odd ;
coherence
not j - i is even
proof end;
end;

registration
let i, j be odd Integer;
cluster i - j -> even ;
coherence
i - j is even
proof end;
end;

registration
let m be even Integer;
cluster m + 2 -> even ;
coherence
m + 2 is even
proof end;
end;

registration
let m be odd Integer;
cluster m + 2 -> odd ;
coherence
not m + 2 is even
proof end;
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
proof end;

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
proof end;

:: from KNASTER, 2005.02.06, A.T.
definition
let x be set ;
let f be Function;
pred x 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 pred a is_a_fixpoint_of f means :Def4: :: ABIAN:def 4
a = f . a;
compatibility
( a is_a_fixpoint_of f iff a = f . a )
proof end;
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;
attr f 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;
attr x 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 )
proof end;

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 )
proof end;
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
proof end;

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 )
proof end;
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
proof end;
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
proof end;

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
proof end;

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
proof end;
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;
cluster f . a -> non empty ;
coherence
not f . a is empty
proof end;
end;

registration
let X be non empty set ;
cluster bool X -> with_non-empty_element ;
coherence
not bool X is empty-membered
proof end;
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 )
proof end;

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 )
proof end;

:: 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)
proof end;

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
proof end;
cluster ext-real V10() V11() V12() V16() complex V18() integer even for set ;
existence
ex b1 being Nat st b1 is even
proof end;
end;

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

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;