:: Abian's Fixed Point Theorem
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 22, 1997
:: Copyright (c) 1997 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;

Lm0: 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 epsilon-transitive epsilon-connected ordinal natural complex V18() integer V56() V57() V58() V59() V60() V61() V62() V74() even Element of NAT ;
existence
ex b₁ being Element of NAT st b₁ is even

proof end;

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer V56() V57() V58() V59() V60() V61() V62() V74() odd Element of NAT ;
existence
not for b₁ being Element of NAT holds b₁ is even

proof end;

cluster ext-real complex V18() integer even set ;
existence
ex b₁ being Integer st b₁ is even

proof end;

cluster ext-real complex V18() integer odd set ;
existence
not for b₁ being Integer holds b₁ is even

proof end;

end;

theorem Th1: :: ABIAN:1

for i being Integer holds
( not i is even 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 Lm0;

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:85;

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;

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;
pred f has_a_fixpoint means :Def5: :: ABIAN:def 5
ex x being set st x is_a_fixpoint_of f;

end;

:: deftheorem Def5 defines has_a_fixpoint ABIAN:def 5 :
for f being Function holds
( f has_a_fixpoint iff ex x being set st x is_a_fixpoint_of f );

notation

let f be Function;
antonym f has_no_fixpoint for f has_a_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 Element of bool (bool E);
existence
ex b₁ being Subset-Family of E st
( not b₁ is empty & b₁ is finite & b₁ 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 has_no_fixpoint

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 b₁ being Equivalence_Relation of E st
for x, y being set st x in E & y in E holds
( [x,y] in b₁ iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of E st ( for x, y being set st x in E & y in E holds
( [x,y] in b₁ 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 b₂ iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines =_ ABIAN:def 7 :
for E being set
for f being Function of E,E
for b₃ being Equivalence_Relation of E holds
( b₃ = =_ f iff for x, y being set st x in E & y in E holds
( [x,y] in b₃ 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 set ;
coherence
for b₁ being set st b₁ is empty-membered holds
b₁ 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 V30(A,B) Element of bool [:A,B:];
existence
ex b₁ being Function of A,B st b₁ 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 has_no_fixpoint 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

theorem :: ABIAN:9

for n being natural number holds
( not n is even iff ex k being Element of NAT st n = (2 * k) + 1 )

proof end;

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 Lm0;

registration

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer odd set ;
existence
not for b₁ being natural number holds b₁ is even

proof end;

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer even set ;
existence
ex b₁ being natural number st b₁ is even

proof end;

end;

theorem Th12: :: ABIAN:12

for n being natural odd number holds 1 <= n

proof end;

registration

cluster integer odd -> non zero set ;
coherence
for b₁ being Integer st not b₁ is even holds
not b₁ is empty by Th12;

end;