:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies POSET_1, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, FUNCT_2, ORDINAL2, FUNCOP_1, SEQM_3, LATTICES, LATTICE3, YELLOW_0, WAYBEL_0, ABIAN, TARSKI, CARD_1, FUNCT_7, NAT_1, SUBSET_1, ORDERS_2, XXREAL_0, STRUCT_0, ARYTM_3, TREES_2, EQREL_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ORDERS_2, ORDERS_3, ORDINAL1, NUMBERS, FUNCT_7, XXREAL_0, XCMPLX_0, YELLOW_2, LATTICE3, YELLOW_0, WAYBEL_0, ABIAN; constructors ORDERS_3, NAT_1, DOMAIN_1, ABIAN, LATTICE3, YELLOW_2, RELSET_1, NUMBERS; registrations XBOOLE_0, ORDINAL1, FUNCT_1, PARTFUN1, STRUCT_0, ORDERS_2, XREAL_0, NAT_1, WAYBEL10, YELLOW_0, WAYBEL24, RELSET_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin registration let P be non empty Poset; :: move to ORDERS_2 cluster non empty for Chain of P; end; definition let IT be RelStr; attr IT is chain-complete means :: POSET_1:def 1 IT is lower-bounded & for L being Chain of IT st L is non empty holds ex_sup_of L,IT; end; theorem :: POSET_1:1 for P1, P2 being non empty Poset, K being non empty Chain of P1, h being monotone Function of P1, P2 holds h.:K is non empty Chain of P2; registration cluster strict chain-complete non empty for Poset; end; registration cluster chain-complete -> lower-bounded for RelStr; end; reserve n,m,k for Nat; reserve x,y,z,X for set; reserve P,Q for strict chain-complete non empty Poset; reserve L for non empty Chain of P; reserve M for non empty Chain of Q; reserve p,p1,p2,p3,p4 for Element of P; reserve q,q1,q2 for Element of Q; reserve f for monotone Function of P,Q; reserve g,g1,g2 for monotone Function of P,P; :: Minimum and sup. theorem :: POSET_1:2 sup (f.:L) <= f.(sup L); begin definition let P be non empty Poset, g be monotone Function of P, P, 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}; end; theorem :: POSET_1:3 iterSet(g,Bottom P) is non empty Chain of P; definition let P; 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); end; theorem :: POSET_1:4 sup iter_min(g) = sup (g.:iter_min(g)); theorem :: POSET_1:5 g1 <= g2 implies sup iter_min(g1) <= sup iter_min(g2); :: 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 be non empty Chain of P holds f preserves_sup_of L; end; theorem :: POSET_1:6 for f being Function of P,Q holds f is continuous iff (f is monotone & for L holds f.(sup L) = sup (f.:L)); theorem :: POSET_1:7 for z being Element of Q holds (P-->z) is continuous; registration let P,Q; cluster continuous for Function of P, Q; end; registration let P,Q; cluster continuous -> monotone for Function of P, Q; end; theorem :: POSET_1:8 for f being monotone Function of P,Q holds (for L holds f.(sup L) <= sup (f.:L)) implies f is continuous; definition let P; let g be monotone Function of P,P; assume g is continuous; func least_fix_point(g) -> Element of P means :: POSET_1:def 5 it is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds it <= p; end; theorem :: POSET_1:9 for g being continuous Function of P,P holds least_fix_point(g) = sup iter_min(g); theorem :: POSET_1:10 for g1,g2 being continuous Function of P,P st g1 <= g2 holds least_fix_point(g1) <= least_fix_point(g2); begin :: 3. Function space of continuous functions on chain-complete Posets definition let P,Q; 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 be continuous Function of P,Q st f=x }; end; definition let P,Q; func ConRelat(P,Q) -> Relation of ConFuncs(P,Q) means :: POSET_1:def 7 for x,y 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); end; registration let P,Q; cluster ConRelat(P,Q) -> reflexive; cluster ConRelat(P,Q) -> transitive; cluster ConRelat(P,Q) -> antisymmetric; end; definition let P,Q; func ConPoset(P,Q) -> strict non empty Poset equals :: POSET_1:def 8 RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#); end; reserve F for non empty Chain of ConPoset(P,Q); definition let P,Q,F,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}; end; definition let P,Q,F; func sup_func(F) -> Function of P,Q means :: POSET_1:def 10 for p,M holds M=F-image p implies it.p=sup M; end; registration let P,Q,F; cluster sup_func(F) -> continuous; end; theorem :: POSET_1:11 ex_sup_of F, ConPoset(P,Q) & sup_func(F) = "\/"(F,ConPoset(P,Q)); definition let P,Q; func min_func(P,Q) -> Function of P,Q equals :: POSET_1:def 11 P --> Bottom Q; end; registration let P,Q; cluster min_func(P,Q) -> continuous; end; theorem :: POSET_1:12 for f being Element of ConPoset(P,Q) st f = min_func(P,Q) holds f is_<=_than the carrier of ConPoset(P,Q); registration let P,Q; cluster ConPoset(P,Q) -> chain-complete; end; begin definition let P; func fix_func(P) -> Function of ConPoset(P,P), P means :: POSET_1:def 12 for g being Element of ConPoset(P,P), h being continuous Function of P, P st g = h holds it.g = least_fix_point h; end; registration let P; cluster fix_func(P) -> continuous; end;