:: Fix-point Theorem for Continuous Functions on Chain-complete Posets :: by Kazuhisa Ishida and Yasunari Shidama :: :: Received November 10, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin Lm1: for f being Function st rng f c= dom f holds iter (f,0) = id (dom f) proofend; Lm2: for f being Function for n being Nat st rng f c= dom f holds ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) proofend; Lm3: for X being set for f being Function of X,X for n being Nat holds iter (f,n) is Function of X,X proofend; 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 proofend; end; Lm4: for A being non empty RelStr for a being Element of A holds ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) proofend; definition let IT be RelStr ; attrIT 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 proofend; registration cluster non empty strict V55() reflexive transitive antisymmetric chain-complete for RelStr ; existence ex b1 being Poset st ( b1 is strict & b1 is chain-complete & not b1 is empty ) proofend; end; registration cluster chain-complete -> lower-bounded for RelStr ; coherence for b1 being RelStr st b1 is chain-complete holds b1 is lower-bounded by Def1; 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) proofend; begin Lm5: 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 proofend; 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 ; proofend; 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 } ; 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 holds (iter (g,n)) . p is Element of P proofend; Lm7: 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) ) proofend; Lm8: for n being Nat for P being non empty strict chain-complete Poset for p, p3, p1, 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 proofend; Lm9: for n, k being Nat for P being non empty strict chain-complete Poset for p3, p, p1, 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 proofend; Lm10: for n, m being Nat for P being non empty strict chain-complete Poset for p3, p, p1, 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 proofend; Lm11: 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 proofend; Lm12: for n being Nat for P being non empty strict chain-complete Poset for p1, p, 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 proofend; 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 proofend; 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)) proofend; 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) proofend; :: Continuous function on chain-complete Poset definition let P, Q be non empty Poset; let f be Function of P,Q; attrf is continuous means :Def4: :: POSET_1:def 4 ( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) ); end; :: deftheorem Def4 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) ) ) ) proofend; theorem Th7: :: POSET_1:7 for Q, P being non empty strict chain-complete Poset for z being Element of Q holds P --> z is continuous proofend; 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 proofend; 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 ; by Def4; 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 proofend; Lm13: 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 proofend; Lm14: 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 proofend; 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 ) ) proofend; 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 proofend; 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 (iter_min g) proofend; 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 proofend; begin :: 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 ; proofend; 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 } ; Lm15: for P, Q being non empty strict chain-complete Poset for f being Function of P,Q holds f <= f proofend; Lm16: 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 proofend; Lm17: 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 proofend; 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 ) ) ) proofend; 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 proofend; 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 ) ) ) ); Lm18: for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q) proofend; Lm19: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q) proofend; Lm20: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) proofend; Lm21: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q) proofend; registration let P, Q be non empty strict chain-complete Poset; cluster ConRelat (P,Q) -> reflexive ; coherence ConRelat (P,Q) is reflexive proofend; cluster ConRelat (P,Q) -> transitive ; coherence ConRelat (P,Q) is transitive proofend; cluster ConRelat (P,Q) -> antisymmetric ; coherence ConRelat (P,Q) is antisymmetric proofend; 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; proofend; 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; funcF -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; proofend; 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 proofend; 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 proofend; 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 ); Lm22: 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 proofend; Lm23: 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 proofend; Lm24: 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 proofend; Lm25: 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 proofend; 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 Lm25; end; Lm26: 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)) proofend; Lm27: 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 proofend; 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))) ) proofend; 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; Lm28: for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q)) proofend; 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)) proofend; 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 proofend; end; begin Lm29: 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 proofend; Lm30: 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)) proofend; 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 proofend; 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 proofend; 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 ); Lm31: 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 ) ) proofend; Lm32: for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P proofend; Lm33: 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) ) proofend; Lm34: 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 proofend; Lm35: 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 proofend; Lm36: 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 proofend; Lm37: 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 proofend; Lm38: 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 proofend; Lm39: 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 proofend; Lm40: 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)) ) proofend; Lm41: 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) proofend; registration let P be non empty strict chain-complete Poset; cluster fix_func P -> continuous ; coherence fix_func P is continuous proofend; end;