:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Copyright (c) 2009-2019 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 b1 being Chain of P holds b1 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
existence
ex b1 being Poset st
( b1 is strict & b1 is chain-complete & not b1 is empty )
proof end;
end;

registration
coherence
for b1 being RelStr st b1 is chain-complete holds
b1 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,()) 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,());
correctness
coherence
iterSet (g,()) 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,());

theorem Th4: :: POSET_1:4
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds sup () = sup (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 b1 being Function of P,Q st b1 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 b1 being Function of P,Q st b1 is continuous holds
b1 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 () 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 () 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 b1 being Element of P st
( b1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b1 <= p ) )
proof end;
uniqueness
for b1, b2 being Element of P st b1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b1 <= p ) & b2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b2 <= p ) holds
b1 = b2
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 b3 being Element of P holds
( b3 = least_fix_point g iff ( b3 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b3 <= 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 ()
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 b1 being Relation of (ConFuncs (P,Q)) st
for x, y being set holds
( [x,y] in b1 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 b1, b2 being Relation of (ConFuncs (P,Q)) st ( for x, y being set holds
( [x,y] in b1 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 b2 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
b1 = b2
proof end;
end;

:: deftheorem Def7 defines ConRelat POSET_1:def 7 :
for P, Q being non empty strict chain-complete Poset
for b3 being Relation of (ConFuncs (P,Q)) holds
( b3 = ConRelat (P,Q) iff for x, y being set holds
( [x,y] in b3 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 ;
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 b1 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
b1 . p = sup M
proof end;
uniqueness
for b1, b2 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
b1 . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b2 . p = sup M ) holds
b1 = b2
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 b4 being Function of P,Q holds
( b4 = sup_func F iff for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b4 . 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));
correctness
coherence ;
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 --> ();
coherence
P --> () 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 --> ();

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 b1 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
b1 . g = least_fix_point h
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . g = least_fix_point h ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines fix_func POSET_1:def 12 :
for P being non empty strict chain-complete Poset
for b2 being Function of (ConPoset (P,P)),P holds
( b2 = fix_func P iff for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b2 . 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)) . () )
}
& 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)) . () )

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)) . () )
}
& 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)) . () )
}
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)) . () )
}
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 = () . g & p1 = (iter (g,n)) . () 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)) . () )
}
& x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . ()) )

proof end;

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

proof end;

registration
let P be non empty strict chain-complete Poset;
coherence
proof end;
end;