:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received November 10, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users

registration

let P be non empty Poset;

cluster non empty strongly_connected for Element of K19( the carrier of P);

existence
not for b₁ being Chain of P holds b₁ is empty

proof end;

end;

definition

let IT be RelStr ;

attr IT is chain-complete means :Def1: :: POSET_1:def 1
( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) );

end;

:: deftheorem Def1 defines chain-complete POSET_1:def 1 :
for IT being RelStr holds
( IT is chain-complete iff ( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) ) );

theorem Th1: :: POSET_1:1

for P1, P2 being non empty Poset
for K being non empty Chain of P1
for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2

proof end;

registration

cluster non empty strict V66() reflexive transitive antisymmetric chain-complete for RelStr ;

existence
ex b₁ being Poset st
( b₁ is strict & b₁ is chain-complete & not b₁ is empty )

proof end;

end;

registration

cluster chain-complete -> lower-bounded for RelStr ;

coherence
for b₁ being RelStr st b₁ is chain-complete holds
b₁ is lower-bounded ;

end;

:: Minimum and sup.

theorem Th2: :: POSET_1:2

for P, Q being non empty strict chain-complete Poset
for L being non empty Chain of P
for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)

proof end;

Lm1: for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds (iter (g,0)) . p = p

proof end;

definition

let P be non empty Poset;
let g be monotone Function of P,P;
let p be Element of P;

func iterSet (g,p) -> non empty set equals :: POSET_1:def 2
{ x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;

correctness
coherence
{ x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is non empty set ;

proof end;

end;

:: deftheorem defines iterSet POSET_1:def 2 :
for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds iterSet (g,p) = { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;

Lm2: for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
by FUNCT_2:15;

Lm3: for n being Nat
for P being non empty strict chain-complete Poset
for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4

proof end;

Lm4: for n, k being Nat
for P being non empty strict chain-complete Poset
for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4

proof end;

Lm5: for n, m being Nat
for P being non empty strict chain-complete Poset
for p, p1, p3, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4

proof end;

Lm6: for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p

proof end;

Lm7: for n being Nat
for P being non empty strict chain-complete Poset
for p, p1, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2

proof end;

theorem Th3: :: POSET_1:3

for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P

proof end;

definition

let P be non empty strict chain-complete Poset;
let g be monotone Function of P,P;

func iter_min g -> non empty Chain of P equals :: POSET_1:def 3
iterSet (g,(Bottom P));

correctness
coherence
iterSet (g,(Bottom P)) is non empty Chain of P;
by Th3;

end;

:: deftheorem defines iter_min POSET_1:def 3 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iter_min g = iterSet (g,(Bottom P));

theorem Th4: :: POSET_1:4

for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))

proof end;

theorem Th5: :: POSET_1:5

for P being non empty strict chain-complete Poset
for g1, g2 being monotone Function of P,P st g1 <= g2 holds
sup (iter_min g1) <= sup (iter_min g2)

proof end;

:: Continuous function on chain-complete Poset

definition

let P, Q be non empty Poset;
let f be Function of P,Q;

attr f is continuous means :: POSET_1:def 4
( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) );

end;

:: deftheorem defines continuous POSET_1:def 4 :
for P, Q being non empty Poset
for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) ) );

theorem Th6: :: POSET_1:6

for P, Q being non empty strict chain-complete Poset
for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )

proof end;

theorem Th7: :: POSET_1:7

for P, Q being non empty strict chain-complete Poset
for z being Element of Q holds P --> z is continuous

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

cluster Relation-like the carrier of P -defined the carrier of Q -valued Function-like quasi_total continuous for Element of K19(K20( the carrier of P, the carrier of Q));

existence
ex b₁ being Function of P,Q st b₁ is continuous

proof end;

end;

registration

let P, Q be non empty strict chain-complete Poset;

cluster Function-like quasi_total continuous -> monotone for Element of K19(K20( the carrier of P, the carrier of Q));

correctness
coherence
for b₁ being Function of P,Q st b₁ is continuous holds
b₁ is monotone ;
;

end;

theorem Th8: :: POSET_1:8

for P, Q being non empty strict chain-complete Poset
for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds
f is continuous

proof end;

Lm8: for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g

proof end;

Lm9: for P being non empty strict chain-complete Poset
for p4 being Element of P
for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p

proof end;

definition

let P be non empty strict chain-complete Poset;
let g be monotone Function of P,P;
assume A1: g is continuous ;

func least_fix_point g -> Element of P means :Def5: :: POSET_1:def 5
( it is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
it <= p ) );

existence
ex b₁ being Element of P st
( b₁ is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b₁ <= p ) )

proof end;

uniqueness
for b₁, b₂ being Element of P st b₁ is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b₁ <= p ) & b₂ is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b₂ <= p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines least_fix_point POSET_1:def 5 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous holds
for b₃ being Element of P holds
( b₃ = least_fix_point g iff ( b₃ is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b₃ <= p ) ) );

theorem Th9: :: POSET_1:9

for P being non empty strict chain-complete Poset
for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)

proof end;

theorem Th10: :: POSET_1:10

for P being non empty strict chain-complete Poset
for g1, g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point g1 <= least_fix_point g2

proof end;

:: 3. Function space of continuous functions on chain-complete Posets

definition

let P, Q be non empty strict chain-complete Poset;

func ConFuncs (P,Q) -> non empty set equals :: POSET_1:def 6
{ x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x } ;

correctness
coherence
{ x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x } is non empty set ;

proof end;

end;

:: deftheorem defines ConFuncs POSET_1:def 6 :
for P, Q being non empty strict chain-complete Poset holds ConFuncs (P,Q) = { x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x } ;

Lm10: for P, Q being non empty strict chain-complete Poset
for f being Function of P,Q holds f <= f

proof end;

Lm11: for P, Q being non empty strict chain-complete Poset
for f, g, h being Function of P,Q st f <= g & g <= h holds
f <= h

proof end;

Lm12: for P, Q being non empty strict chain-complete Poset
for f, g being Function of P,Q st f <= g & g <= f holds
f = g

proof end;

definition

let P, Q be non empty strict chain-complete Poset;

func ConRelat (P,Q) -> Relation of (ConFuncs (P,Q)) means :Def7: :: POSET_1:def 7
for x, y being set holds
( [x,y] in it iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) );

existence
ex b₁ being Relation of (ConFuncs (P,Q)) st
for x, y being set holds
( [x,y] in b₁ iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (ConFuncs (P,Q)) st ( for x, y being set holds
( [x,y] in b₁ iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds
( [x,y] in b₂ iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ConRelat POSET_1:def 7 :
for P, Q being non empty strict chain-complete Poset
for b₃ being Relation of (ConFuncs (P,Q)) holds
( b₃ = ConRelat (P,Q) iff for x, y being set holds
( [x,y] in b₃ iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) );

Lm13: for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q)

proof end;

Lm14: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)

proof end;

Lm15: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q)

proof end;

Lm16: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

cluster ConRelat (P,Q) -> reflexive ;

coherence
ConRelat (P,Q) is reflexive

proof end;

cluster ConRelat (P,Q) -> transitive ;

coherence
ConRelat (P,Q) is transitive

proof end;

cluster ConRelat (P,Q) -> antisymmetric ;

coherence
ConRelat (P,Q) is antisymmetric

proof end;

end;

definition

let P, Q be non empty strict chain-complete Poset;

func ConPoset (P,Q) -> non empty strict Poset equals :: POSET_1:def 8
RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

correctness
coherence
RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset;
by Lm14, Lm15, Lm16, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

end;

:: deftheorem defines ConPoset POSET_1:def 8 :
for P, Q being non empty strict chain-complete Poset holds ConPoset (P,Q) = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

definition

let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));
let p be Element of P;

func F -image p -> non empty Chain of Q equals :: POSET_1:def 9
{ x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } ;

correctness
coherence
{ x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } is non empty Chain of Q;

proof end;

end;

:: deftheorem defines -image POSET_1:def 9 :
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for p being Element of P holds F -image p = { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } ;

definition

let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));

func sup_func F -> Function of P,Q means :Def10: :: POSET_1:def 10
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
it . p = sup M;

existence
ex b₁ being Function of P,Q st
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₁ . p = sup M

proof end;

uniqueness
for b₁, b₂ being Function of P,Q st ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₁ . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₂ . p = sup M ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines sup_func POSET_1:def 10 :
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for b₄ being Function of P,Q holds
( b₄ = sup_func F iff for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₄ . p = sup M );

Lm17: for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is monotone

proof end;

Lm18: for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q being Element of Q st q in M holds
q <= sup M

proof end;

Lm19: for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1

proof end;

Lm20: for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous

proof end;

registration

let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));

cluster sup_func F -> continuous ;

correctness
coherence
sup_func F is continuous ;
by Lm20;

end;

Lm21: for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is Element of (ConPoset (P,Q))

proof end;

Lm22: for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for x being set st x in F holds
ex g being continuous Function of P,Q st x = g

proof end;

theorem Th11: :: POSET_1:11

for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )

proof end;

definition

let P, Q be non empty strict chain-complete Poset;

func min_func (P,Q) -> Function of P,Q equals :: POSET_1:def 11
P --> (Bottom Q);

coherence
P --> (Bottom Q) is Function of P,Q ;

end;

:: deftheorem defines min_func POSET_1:def 11 :
for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) = P --> (Bottom Q);

registration

let P, Q be non empty strict chain-complete Poset;

cluster min_func (P,Q) -> continuous ;

coherence
min_func (P,Q) is continuous by Th7;

end;

Lm23: for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q))

proof end;

theorem Th12: :: POSET_1:12

for P, Q being non empty strict chain-complete Poset
for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds
f is_<=_than the carrier of (ConPoset (P,Q))

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

cluster ConPoset (P,Q) -> non empty strict chain-complete ;

coherence
ConPoset (P,Q) is chain-complete

proof end;

end;

Lm24: for x being set
for P being non empty strict chain-complete Poset st x is Element of (ConPoset (P,P)) holds
x is continuous Function of P,P

proof end;

Lm25: for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous Function of P,P holds
g is Element of (ConPoset (P,P))

proof end;

definition

let P be non empty strict chain-complete Poset;

func fix_func P -> Function of (ConPoset (P,P)),P means :Def12: :: POSET_1:def 12
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
it . g = least_fix_point h;

existence
ex b₁ being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₁ . g = least_fix_point h

proof end;

uniqueness
for b₁, b₂ being Function of (ConPoset (P,P)),P st ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₁ . g = least_fix_point h ) & ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₂ . g = least_fix_point h ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines fix_func POSET_1:def 12 :
for P being non empty strict chain-complete Poset
for b₂ being Function of (ConPoset (P,P)),P holds
( b₂ = fix_func P iff for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₂ . g = least_fix_point h );

Lm26: for P being non empty strict chain-complete Poset
for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )

proof end;

Lm27: for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P

proof end;

Lm28: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X, x being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )

proof end;

Lm29: for x being set
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in X holds
x is Element of P

proof end;

Lm30: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } holds
X is non empty Subset of P

proof end;

Lm31: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f

proof end;

Lm32: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } holds
X is non empty Chain of P

proof end;

Lm33: for P being non empty strict chain-complete Poset
for h being Function of (ConPoset (P,P)),P
for G being non empty Chain of (ConPoset (P,P))
for x being set st x in G holds
h . x in h .: G

proof end;

Lm34: for P being non empty strict chain-complete Poset
for g being continuous Function of P,P
for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p

proof end;

Lm35: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )

proof end;

Lm36: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)

proof end;

registration

let P be non empty strict chain-complete Poset;

cluster fix_func P -> continuous ;

coherence
fix_func P is continuous

proof end;

end;