:: POSET_1 semantic presentation begin Lm1: for f being Function st rng f c= dom f holds iter (f,0) = id (dom f) proof let f be Function; ::_thesis: ( rng f c= dom f implies iter (f,0) = id (dom f) ) assume rng f c= dom f ; ::_thesis: iter (f,0) = id (dom f) then field f = dom f by XBOOLE_1:12; hence iter (f,0) = id (dom f) by FUNCT_7:68; ::_thesis: verum end; 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 ) proof let f be Function; ::_thesis: for n being Nat st rng f c= dom f holds ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) let n be Nat; ::_thesis: ( rng f c= dom f implies ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) ) defpred S1[ Nat] means ( dom (iter (f,\$1)) = dom f & rng (iter (f,\$1)) c= dom f ); assume rng f c= dom f ; ::_thesis: ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) then iter (f,0) = id (dom f) by Lm1; then A1: S1[ 0 ] by RELAT_1:45; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: ( dom (iter (f,k)) = dom f & rng (iter (f,k)) c= dom f ) ; ::_thesis: S1[k + 1] ( iter (f,(k + 1)) = f * (iter (f,k)) & iter (f,(k + 1)) = (iter (f,k)) * f ) by FUNCT_7:69, FUNCT_7:71; then ( dom (iter (f,(k + 1))) = dom (iter (f,k)) & rng (iter (f,(k + 1))) c= rng (iter (f,k)) ) by A3, RELAT_1:26, RELAT_1:27; hence S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); hence ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) ; ::_thesis: verum end; 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 proof let X be set ; ::_thesis: for f being Function of X,X for n being Nat holds iter (f,n) is Function of X,X let f be Function of X,X; ::_thesis: for n being Nat holds iter (f,n) is Function of X,X let n be Nat; ::_thesis: iter (f,n) is Function of X,X A1: ( X = {} implies X = {} ) ; then A2: ( dom f = X & rng f c= X ) by FUNCT_2:def_1; then ( dom (iter (f,n)) = X & rng (iter (f,n)) c= X ) by Lm2; then reconsider R = iter (f,n) as Relation of X,X by RELSET_1:4; ( dom R = X & rng R c= X ) by A2, Lm2; hence iter (f,n) is Function of X,X by A1, FUNCT_2:def_1; ::_thesis: verum end; 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 not for L being Chain of P holds L is empty proof set z = the Element of P; set IT = { the Element of P}; reconsider IT = { the Element of P} as Chain of P by ORDERS_2:8; not IT is empty ; hence not for L being Chain of P holds L is empty ; ::_thesis: verum end; hence not for b1 being Chain of P holds b1 is empty ; ::_thesis: verum end; 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 ) proof let A be non empty RelStr ; ::_thesis: for a being Element of A holds ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) let a be Element of A; ::_thesis: ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) ( ( for x being Element of A holds a <= x ) implies a is_<=_than the carrier of A ) proof assume A1: for x being Element of A holds a <= x ; ::_thesis: a is_<=_than the carrier of A a is_<=_than the carrier of A proof let x be Element of A; :: according to LATTICE3:def_8 ::_thesis: ( not x in the carrier of A or a <= x ) thus ( not x in the carrier of A or a <= x ) by A1; ::_thesis: verum end; hence a is_<=_than the carrier of A ; ::_thesis: verum end; hence ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) by LATTICE3:def_8; ::_thesis: verum end; 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 proof let P1, P2 be non empty Poset; ::_thesis: 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 let K be non empty Chain of P1; ::_thesis: for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2 let h be monotone Function of P1,P2; ::_thesis: h .: K is non empty Chain of P2 set R = the InternalRel of P2; set K2 = h .: K; for x, y being set st x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 holds [y,x] in the InternalRel of P2 proof let x, y be set ; ::_thesis: ( x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 implies [y,x] in the InternalRel of P2 ) assume A1: ( x in h .: K & y in h .: K & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 ) then reconsider x = x, y = y as Element of P2 ; consider a being set such that A2: ( a in dom h & a in K & x = h . a ) by A1, FUNCT_1:def_6; consider b being set such that A3: ( b in dom h & b in K & y = h . b ) by A1, FUNCT_1:def_6; reconsider a = a, b = b as Element of P1 by A2, A3; ( a <= b or b <= a ) by A2, A3, ORDERS_2:11; then ( x <= y or y <= x ) by A2, A3, ORDERS_3:def_5; hence ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 ) by ORDERS_2:def_5; ::_thesis: verum end; then A4: the InternalRel of P2 is_connected_in h .: K by RELAT_2:def_6; for x being set st x in h .: K holds [x,x] in the InternalRel of P2 proof let x be set ; ::_thesis: ( x in h .: K implies [x,x] in the InternalRel of P2 ) assume x in h .: K ; ::_thesis: [x,x] in the InternalRel of P2 then reconsider x = x as Element of P2 ; x <= x ; hence [x,x] in the InternalRel of P2 by ORDERS_2:def_5; ::_thesis: verum end; then the InternalRel of P2 is_reflexive_in h .: K by RELAT_2:def_1; then the InternalRel of P2 is_strongly_connected_in h .: K by A4, ORDERS_1:7; then reconsider K2 = h .: K as Chain of P2 by ORDERS_2:def_7; consider a being set such that A5: a in K by XBOOLE_0:7; a in the carrier of P1 by A5; then a in dom h by FUNCT_2:def_1; then h . a in K2 by A5, FUNCT_1:def_6; hence h .: K is non empty Chain of P2 ; ::_thesis: verum end; 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 ) proof set z = the set ; set A = { the set }; reconsider R = id { the set } as Relation of { the set } ; reconsider R = R as Order of { the set } ; take IT = RelStr(# { the set },R #); ::_thesis: ( IT is strict & IT is chain-complete & not IT is empty ) reconsider z = the set as Element of IT by TARSKI:def_1; for L being Chain of IT st not L is empty holds ex_sup_of L,IT proof let L be Chain of IT; ::_thesis: ( not L is empty implies ex_sup_of L,IT ) assume not L is empty ; ::_thesis: ex_sup_of L,IT for x being Element of IT st x in L holds x <= z by TARSKI:def_1; then A1: L is_<=_than z by LATTICE3:def_9; for y being Element of IT st L is_<=_than y holds z <= y by TARSKI:def_1; hence ex_sup_of L,IT by A1, YELLOW_0:15; ::_thesis: verum end; hence ( IT is strict & IT is chain-complete & not IT is empty ) by Def1; ::_thesis: verum end; 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; 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 let P, Q be non empty strict chain-complete Poset; ::_thesis: for L being non empty Chain of P for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L) let L be non empty Chain of P; ::_thesis: for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L) let f be monotone Function of P,Q; ::_thesis: sup (f .: L) <= f . (sup L) reconsider M = f .: L as non empty Chain of Q by Th1; set r = sup L; set u = f . (sup L); A1: ( ex_sup_of L,P & ex_sup_of M,Q ) by Def1; for q being Element of Q st q in M holds q <= f . (sup L) proof let q be Element of Q; ::_thesis: ( q in M implies q <= f . (sup L) ) assume q in M ; ::_thesis: q <= f . (sup L) then consider x being set such that A2: ( x in dom f & x in L & q = f . x ) by FUNCT_1:def_6; reconsider x = x as Element of P by A2; L is_<=_than sup L by A1, YELLOW_0:def_9; then x <= sup L by A2, LATTICE3:def_9; hence q <= f . (sup L) by A2, ORDERS_3:def_5; ::_thesis: verum end; then M is_<=_than f . (sup L) by LATTICE3:def_9; hence sup (f .: L) <= f . (sup L) by A1, YELLOW_0:def_9; ::_thesis: verum end; 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 proof let P be non empty Poset; ::_thesis: for g being monotone Function of P,P for p being Element of P holds (iter (g,0)) . p = p let g be monotone Function of P,P; ::_thesis: for p being Element of P holds (iter (g,0)) . p = p let p be Element of P; ::_thesis: (iter (g,0)) . p = p set X = the carrier of P; (iter (g,0)) . p = (id the carrier of P) . p by FUNCT_7:84 .= p by FUNCT_1:18 ; hence (iter (g,0)) . p = p ; ::_thesis: verum 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 set IT = { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ; not { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is empty proof (iter (g,0)) . p = p by Lm5; then p in { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ; hence not { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is empty ; ::_thesis: verum end; hence { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is non empty set ; ::_thesis: verum 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 } ; 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 proof let n be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: for p being Element of P for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P let p be Element of P; ::_thesis: for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P let g be monotone Function of P,P; ::_thesis: (iter (g,n)) . p is Element of P set X = the carrier of P; reconsider g1 = iter (g,n) as Function of the carrier of P, the carrier of P by Lm3; g1 . p in the carrier of P ; hence (iter (g,n)) . p is Element of P ; ::_thesis: verum end; 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) ) proof let n be Nat; ::_thesis: 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) ) let P be non empty strict chain-complete Poset; ::_thesis: 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) ) let p be Element of P; ::_thesis: 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) ) let g be monotone Function of P,P; ::_thesis: ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) ) set X = the carrier of P; reconsider g1 = iter (g,n) as Function of the carrier of P, the carrier of P by Lm3; ( (g * g1) . p = g . (g1 . p) & (g1 * g) . p = g1 . (g . p) ) by FUNCT_2:15; hence ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) ) ; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let p, p3, p1, p4 be Element of P; ::_thesis: for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds p1 <= p4 let g be monotone Function of P,P; ::_thesis: ( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 ) defpred S1[ Nat] means for p, p3, p1, p4 being Element of P st p <= p3 & p1 = (iter (g,\$1)) . p & p4 = (iter (g,\$1)) . p3 holds p1 <= p4; A1: S1[ 0 ] proof let p, p3, p1, p4 be Element of P; ::_thesis: ( p <= p3 & p1 = (iter (g,0)) . p & p4 = (iter (g,0)) . p3 implies p1 <= p4 ) assume ( p <= p3 & p1 = (iter (g,0)) . p & p4 = (iter (g,0)) . p3 ) ; ::_thesis: p1 <= p4 then ( p <= p3 & p1 = p & p4 = p3 ) by Lm5; hence p1 <= p4 ; ::_thesis: verum end; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: for p, p3, p1, p4 being Element of P st p <= p3 & p1 = (iter (g,k)) . p & p4 = (iter (g,k)) . p3 holds p1 <= p4 ; ::_thesis: S1[k + 1] S1[k + 1] proof let p, p3, p1, p4 be Element of P; ::_thesis: ( p <= p3 & p1 = (iter (g,(k + 1))) . p & p4 = (iter (g,(k + 1))) . p3 implies p1 <= p4 ) assume A4: ( p <= p3 & p1 = (iter (g,(k + 1))) . p & p4 = (iter (g,(k + 1))) . p3 ) ; ::_thesis: p1 <= p4 reconsider x1 = (iter (g,k)) . p as Element of P by Lm6; reconsider y1 = (iter (g,k)) . p3 as Element of P by Lm6; A5: x1 <= y1 by A4, A3; iter (g,(k + 1)) = g * (iter (g,k)) by FUNCT_7:71; then ( p1 = g . ((iter (g,k)) . p) & p4 = g . ((iter (g,k)) . p3) ) by Lm7, A4; hence p1 <= p4 by A5, ORDERS_3:def_5; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); hence ( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 ) ; ::_thesis: verum end; 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 proof let n, k be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let p3, p, p1, p4 be Element of P; ::_thesis: 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 let g be monotone Function of P,P; ::_thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 ) defpred S1[ Nat] means for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + \$1))) . p holds p1 <= p4; A1: S1[ 0 ] ; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds p1 <= p4 ; ::_thesis: S1[k + 1] S1[k + 1] proof let p, p3, p1, p4 be Element of P; ::_thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p implies p1 <= p4 ) assume A4: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p ) ; ::_thesis: p1 <= p4 reconsider y1 = (iter (g,(n + k))) . p as Element of P by Lm6; A5: p1 <= y1 by A4, A3; iter (g,(n + (k + 1))) = iter (g,((n + k) + 1)) .= (iter (g,(n + k))) * g by FUNCT_7:69 ; then p4 = (iter (g,(n + k))) . p3 by Lm7, A4; then y1 <= p4 by A4, Lm8; hence p1 <= p4 by A5, ORDERS_2:3; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); hence ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 ) ; ::_thesis: verum end; 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 proof let n, m be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let p3, p, p1, p4 be Element of P; ::_thesis: 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 let g be monotone Function of P,P; ::_thesis: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p implies p1 <= p4 ) assume A1: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p ) ; ::_thesis: p1 <= p4 then consider k being Nat such that A2: m = n + k by NAT_1:10; thus p1 <= p4 by A1, A2, Lm9; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let p be Element of P; ::_thesis: for g being monotone Function of P,P st p is_a_fixpoint_of g holds (iter (g,n)) . p = p let g be monotone Function of P,P; ::_thesis: ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p ) defpred S1[ Nat] means for p being Element of P st p is_a_fixpoint_of g holds (iter (g,\$1)) . p = p; A1: S1[ 0 ] by Lm5; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] S1[k + 1] proof let p be Element of P; ::_thesis: ( p is_a_fixpoint_of g implies (iter (g,(k + 1))) . p = p ) assume A4: p is_a_fixpoint_of g ; ::_thesis: (iter (g,(k + 1))) . p = p iter (g,(k + 1)) = g * (iter (g,k)) by FUNCT_7:71; then (iter (g,(k + 1))) . p = g . ((iter (g,k)) . p) by Lm7 .= g . p by A4, A3 .= p by A4, ABIAN:def_3 ; hence (iter (g,(k + 1))) . p = p ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); hence ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p ) ; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let p1, p, p2 be Element of P; ::_thesis: 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 let g1, g2 be monotone Function of P,P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 ) defpred S1[ Nat] means for p, p1, p2 being Element of P st g1 <= g2 & p1 = (iter (g1,\$1)) . p & p2 = (iter (g2,\$1)) . p holds p1 <= p2; A1: S1[ 0 ] proof let p, p1, p2 be Element of P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,0)) . p & p2 = (iter (g2,0)) . p implies p1 <= p2 ) assume ( g1 <= g2 & p1 = (iter (g1,0)) . p & p2 = (iter (g2,0)) . p ) ; ::_thesis: p1 <= p2 then ( p1 = p & p2 = p ) by Lm5; hence p1 <= p2 ; ::_thesis: verum end; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] S1[k + 1] proof let p, p1, p2 be Element of P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,(k + 1))) . p & p2 = (iter (g2,(k + 1))) . p implies p1 <= p2 ) assume A4: ( g1 <= g2 & p1 = (iter (g1,(k + 1))) . p & p2 = (iter (g2,(k + 1))) . p ) ; ::_thesis: p1 <= p2 reconsider q1 = (iter (g1,k)) . p as Element of P by Lm6; reconsider q2 = (iter (g2,k)) . p as Element of P by Lm6; set r = g1 . q2; A5: q1 <= q2 by A4, A3; iter (g1,(k + 1)) = g1 * (iter (g1,k)) by FUNCT_7:71; then A6: p1 = g1 . q1 by Lm7, A4; iter (g2,(k + 1)) = g2 * (iter (g2,k)) by FUNCT_7:71; then A7: p2 = g2 . q2 by Lm7, A4; A8: p1 <= g1 . q2 by A5, A6, ORDERS_3:def_5; g1 . q2 <= p2 by A4, A7, YELLOW_2:9; hence p1 <= p2 by A8, ORDERS_2:3; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); hence ( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 ) ; ::_thesis: verum 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 let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P let g be monotone Function of P,P; ::_thesis: iterSet (g,(Bottom P)) is non empty Chain of P set a = Bottom P; set R = the InternalRel of P; set L = iterSet (g,(Bottom P)); A1: for x being set st x in iterSet (g,(Bottom P)) holds x is Element of P proof let x be set ; ::_thesis: ( x in iterSet (g,(Bottom P)) implies x is Element of P ) assume x in iterSet (g,(Bottom P)) ; ::_thesis: x is Element of P then consider y being Element of P such that A2: ( x = y & ex n being Nat st y = (iter (g,n)) . (Bottom P) ) ; thus x is Element of P by A2; ::_thesis: verum end; for x being set st x in iterSet (g,(Bottom P)) holds x in the carrier of P proof let x be set ; ::_thesis: ( x in iterSet (g,(Bottom P)) implies x in the carrier of P ) assume x in iterSet (g,(Bottom P)) ; ::_thesis: x in the carrier of P then x is Element of the carrier of P by A1; hence x in the carrier of P ; ::_thesis: verum end; then reconsider L = iterSet (g,(Bottom P)) as Subset of P by TARSKI:def_3; for x, y being set st x in L & y in L & x <> y & not [x,y] in the InternalRel of P holds [y,x] in the InternalRel of P proof let x, y be set ; ::_thesis: ( x in L & y in L & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P ) assume A3: ( x in L & y in L & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) then reconsider x = x, y = y as Element of P ; consider p being Element of P such that A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) by A3; consider p1 being Element of P such that A5: ( y = p1 & ex m being Nat st p1 = (iter (g,m)) . (Bottom P) ) by A3; consider n being Nat such that A6: p = (iter (g,n)) . (Bottom P) by A4; consider m being Nat such that A7: p1 = (iter (g,m)) . (Bottom P) by A5; ( p <= p1 or p1 <= p ) proof set a1 = (iter (g,1)) . (Bottom P); A8: (iter (g,1)) . (Bottom P) = g . (Bottom P) by FUNCT_7:70; percases ( n <= m or m <= n ) ; suppose n <= m ; ::_thesis: ( p <= p1 or p1 <= p ) hence ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm10, YELLOW_0:44; ::_thesis: verum end; suppose m <= n ; ::_thesis: ( p <= p1 or p1 <= p ) hence ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm10, YELLOW_0:44; ::_thesis: verum end; end; end; hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4, A5, ORDERS_2:def_5; ::_thesis: verum end; then A9: the InternalRel of P is_connected_in L by RELAT_2:def_6; for x being set st x in L holds [x,x] in the InternalRel of P proof let x be set ; ::_thesis: ( x in L implies [x,x] in the InternalRel of P ) assume x in L ; ::_thesis: [x,x] in the InternalRel of P then reconsider x = x as Element of P ; x <= x ; hence [x,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum end; then the InternalRel of P is_reflexive_in L by RELAT_2:def_1; then the InternalRel of P is_strongly_connected_in L by A9, ORDERS_1:7; then reconsider L = L as Chain of P by ORDERS_2:def_7; L is non empty Chain of P ; hence iterSet (g,(Bottom P)) is non empty Chain of P ; ::_thesis: verum 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 let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g)) let g be monotone Function of P,P; ::_thesis: sup (iter_min g) = sup (g .: (iter_min g)) reconsider L = g .: (iter_min g) as non empty Chain of P by Th1; A1: ( ex_sup_of iter_min g,P & ex_sup_of L,P ) by Def1; set a = Bottom P; set s1 = sup (iter_min g); set s2 = sup L; A2: iter_min g is_<=_than sup (iter_min g) by A1, YELLOW_0:def_9; A3: L is_<=_than sup L by A1, YELLOW_0:def_9; for x being Element of P st x in iter_min g holds x <= sup L proof let x be Element of P; ::_thesis: ( x in iter_min g implies x <= sup L ) assume x in iter_min g ; ::_thesis: x <= sup L then consider p being Element of P such that A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) ; consider n being Nat such that A5: p = (iter (g,n)) . (Bottom P) by A4; A6: ( 1 <= n implies p in L ) proof assume 1 <= n ; ::_thesis: p in L then consider k being Nat such that A7: n = 1 + k by NAT_1:10; reconsider z = (iter (g,k)) . (Bottom P) as Element of P by Lm6; z in the carrier of P ; then A8: ( z in dom g & z in iter_min g ) by FUNCT_2:def_1; p = (g * (iter (g,k))) . (Bottom P) by A5, A7, FUNCT_7:71 .= g . z by Lm7 ; hence p in L by A8, FUNCT_1:def_6; ::_thesis: verum end; ( n = 0 implies p = Bottom P ) by A5, Lm5; hence x <= sup L by A6, A4, A3, LATTICE3:def_9, NAT_1:14, YELLOW_0:44; ::_thesis: verum end; then iter_min g is_<=_than sup L by LATTICE3:def_9; then A9: sup (iter_min g) <= sup L by A1, YELLOW_0:30; for x being Element of P st x in L holds x <= sup (iter_min g) proof let x be Element of P; ::_thesis: ( x in L implies x <= sup (iter_min g) ) assume x in L ; ::_thesis: x <= sup (iter_min g) then consider z being set such that A10: ( z in dom g & z in iter_min g & x = g . z ) by FUNCT_1:def_6; consider z1 being Element of P such that A11: ( z = z1 & ex n being Nat st z1 = (iter (g,n)) . (Bottom P) ) by A10; consider n being Nat such that A12: z1 = (iter (g,n)) . (Bottom P) by A11; set n1 = n + 1; g . z = (g * (iter (g,n))) . (Bottom P) by Lm7, A11, A12 .= (iter (g,(n + 1))) . (Bottom P) by FUNCT_7:71 ; then x in iterSet (g,(Bottom P)) by A10; hence x <= sup (iter_min g) by A2, LATTICE3:def_9; ::_thesis: verum end; then L is_<=_than sup (iter_min g) by LATTICE3:def_9; then sup L <= sup (iter_min g) by A1, YELLOW_0:def_9; hence sup (iter_min g) = sup (g .: (iter_min g)) by A9, ORDERS_2:2; ::_thesis: verum 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 let P be non empty strict chain-complete Poset; ::_thesis: for g1, g2 being monotone Function of P,P st g1 <= g2 holds sup (iter_min g1) <= sup (iter_min g2) let g1, g2 be monotone Function of P,P; ::_thesis: ( g1 <= g2 implies sup (iter_min g1) <= sup (iter_min g2) ) assume A1: g1 <= g2 ; ::_thesis: sup (iter_min g1) <= sup (iter_min g2) set p2 = sup (iter_min g2); set a = Bottom P; A2: ( ex_sup_of iter_min g1,P & ex_sup_of iter_min g2,P ) by Def1; then A3: iter_min g2 is_<=_than sup (iter_min g2) by YELLOW_0:def_9; for x being Element of P st x in iter_min g1 holds x <= sup (iter_min g2) proof let x be Element of P; ::_thesis: ( x in iter_min g1 implies x <= sup (iter_min g2) ) assume x in iter_min g1 ; ::_thesis: x <= sup (iter_min g2) then consider p being Element of P such that A4: ( x = p & ex n being Nat st p = (iter (g1,n)) . (Bottom P) ) ; consider n being Nat such that A5: p = (iter (g1,n)) . (Bottom P) by A4; reconsider y = (iter (g2,n)) . (Bottom P) as Element of P by Lm6; y in iter_min g2 ; then A6: y <= sup (iter_min g2) by A3, LATTICE3:def_9; p <= y by A1, A5, Lm12; hence x <= sup (iter_min g2) by A4, A6, ORDERS_2:3; ::_thesis: verum end; then iter_min g1 is_<=_than sup (iter_min g2) by LATTICE3:def_9; hence sup (iter_min g1) <= sup (iter_min g2) by A2, YELLOW_0:30; ::_thesis: verum end; 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) ) ) ) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: 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) ) ) ) let f be Function of P,Q; ::_thesis: ( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) ) thus ( f is continuous implies ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) ) ::_thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) implies f is continuous ) proof assume A1: f is continuous ; ::_thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) for L being non empty Chain of P holds f . (sup L) = sup (f .: L) proof let L be non empty Chain of P; ::_thesis: f . (sup L) = sup (f .: L) A2: f preserves_sup_of L by A1, Def4; ex_sup_of L,P by Def1; hence f . (sup L) = sup (f .: L) by A2, WAYBEL_0:def_31; ::_thesis: verum end; hence ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) by A1, Def4; ::_thesis: verum end; assume that A3: f is monotone and A4: for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ; ::_thesis: f is continuous for L being non empty Chain of P holds f preserves_sup_of L proof let L be non empty Chain of P; ::_thesis: f preserves_sup_of L reconsider M = f .: L as non empty Chain of Q by A3, Th1; ( ex_sup_of M,Q & f . (sup L) = sup M ) by Def1, A4; hence f preserves_sup_of L by WAYBEL_0:def_31; ::_thesis: verum end; hence f is continuous by A3, Def4; ::_thesis: verum end; 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 proof let Q, P be non empty strict chain-complete Poset; ::_thesis: for z being Element of Q holds P --> z is continuous let z be Element of Q; ::_thesis: P --> z is continuous set IT = P --> z; for L being non empty Chain of P holds (P --> z) . (sup L) = sup ((P --> z) .: L) proof let L be non empty Chain of P; ::_thesis: (P --> z) . (sup L) = sup ((P --> z) .: L) set M = (P --> z) .: L; for x being Element of Q st x in (P --> z) .: L holds x <= z proof let x be Element of Q; ::_thesis: ( x in (P --> z) .: L implies x <= z ) assume x in (P --> z) .: L ; ::_thesis: x <= z then consider a being set such that A1: ( a in dom (P --> z) & a in L & x = (P --> z) . a ) by FUNCT_1:def_6; thus x <= z by A1, FUNCOP_1:7; ::_thesis: verum end; then A2: (P --> z) .: L is_<=_than z by LATTICE3:def_9; for y being Element of Q st (P --> z) .: L is_<=_than y holds z <= y proof let y be Element of Q; ::_thesis: ( (P --> z) .: L is_<=_than y implies z <= y ) assume A3: (P --> z) .: L is_<=_than y ; ::_thesis: z <= y consider a being set such that A4: a in L by XBOOLE_0:def_1; a in the carrier of P by A4; then A5: a in dom (P --> z) by FUNCOP_1:13; (P --> z) . a = z by A4, FUNCOP_1:7; then z in (P --> z) .: L by A4, A5, FUNCT_1:def_6; hence z <= y by A3, LATTICE3:def_9; ::_thesis: verum end; then z = "\/" (((P --> z) .: L),Q) by A2, YELLOW_0:30; hence (P --> z) . (sup L) = sup ((P --> z) .: L) by FUNCOP_1:7; ::_thesis: verum end; hence P --> z is continuous by Th6; ::_thesis: verum 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 set z = the Element of Q; take P --> the Element of Q ; ::_thesis: P --> the Element of Q is continuous thus P --> the Element of Q is continuous by Th7; ::_thesis: verum 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 ; 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: 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 let f be monotone Function of P,Q; ::_thesis: ( ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) implies f is continuous ) assume A1: for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ; ::_thesis: f is continuous for L being non empty Chain of P holds f . (sup L) = sup (f .: L) proof let L be non empty Chain of P; ::_thesis: f . (sup L) = sup (f .: L) set a1 = f . (sup L); set a2 = sup (f .: L); A2: sup (f .: L) <= f . (sup L) by Th2; f . (sup L) <= sup (f .: L) by A1; hence f . (sup L) = sup (f .: L) by A2, ORDERS_2:2; ::_thesis: verum end; hence f is continuous by Th6; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let p be Element of P; ::_thesis: for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds p is_a_fixpoint_of g let g be monotone Function of P,P; ::_thesis: ( g is continuous & p = sup (iter_min g) implies p is_a_fixpoint_of g ) A1: dom g = the carrier of P by FUNCT_2:def_1; reconsider L = g .: (iter_min g) as non empty Chain of P by Th1; assume A2: ( g is continuous & p = sup (iter_min g) ) ; ::_thesis: p is_a_fixpoint_of g then g . p = sup L by Th6 .= p by A2, Th4 ; hence p is_a_fixpoint_of g by A1, ABIAN:def_3; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let p4 be Element of P; ::_thesis: 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 let g be monotone Function of P,P; ::_thesis: ( p4 = sup (iter_min g) implies for p being Element of P st p is_a_fixpoint_of g holds p4 <= p ) assume A1: p4 = sup (iter_min g) ; ::_thesis: for p being Element of P st p is_a_fixpoint_of g holds p4 <= p for p being Element of P st p is_a_fixpoint_of g holds p4 <= p proof let p be Element of P; ::_thesis: ( p is_a_fixpoint_of g implies p4 <= p ) assume A2: p is_a_fixpoint_of g ; ::_thesis: p4 <= p set M = iter_min g; set a = Bottom P; A3: ex_sup_of iter_min g,P by Def1; for p1 being Element of P st p1 in iter_min g holds p1 <= p proof let p1 be Element of P; ::_thesis: ( p1 in iter_min g implies p1 <= p ) assume p1 in iter_min g ; ::_thesis: p1 <= p then consider p2 being Element of P such that A4: ( p1 = p2 & ex n being Nat st p2 = (iter (g,n)) . (Bottom P) ) ; consider n being Nat such that A5: p1 = (iter (g,n)) . (Bottom P) by A4; reconsider q = (iter (g,n)) . p as Element of P by Lm6; p1 <= q by A5, Lm8, YELLOW_0:44; hence p1 <= p by A2, Lm11; ::_thesis: verum end; then iter_min g is_<=_than p by LATTICE3:def_9; hence p4 <= p by A3, A1, YELLOW_0:def_9; ::_thesis: verum end; hence for p being Element of P st p is_a_fixpoint_of g holds p4 <= p ; ::_thesis: verum 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 set IT = sup (iter_min g); take sup (iter_min g) ; ::_thesis: ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds sup (iter_min g) <= p ) ) thus ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds sup (iter_min g) <= p ) ) by A1, Lm13, Lm14; ::_thesis: verum 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 let p1, p2 be Element of P; ::_thesis: ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds p2 <= p ) implies p1 = p2 ) assume ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds p2 <= p ) ) ; ::_thesis: p1 = p2 then ( p1 <= p2 & p2 <= p1 ) ; hence p1 = p2 by ORDERS_2:2; ::_thesis: verum 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 (iter_min g) proof let P be non empty strict chain-complete Poset; ::_thesis: for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g) let g be continuous Function of P,P; ::_thesis: least_fix_point g = sup (iter_min g) set p = sup (iter_min g); set q = least_fix_point g; sup (iter_min g) is_a_fixpoint_of g by Lm13; then A1: least_fix_point g <= sup (iter_min g) by Def5; least_fix_point g is_a_fixpoint_of g by Def5; then sup (iter_min g) <= least_fix_point g by Lm14; hence least_fix_point g = sup (iter_min g) by A1, ORDERS_2:2; ::_thesis: verum 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 let P be non empty strict chain-complete Poset; ::_thesis: for g1, g2 being continuous Function of P,P st g1 <= g2 holds least_fix_point g1 <= least_fix_point g2 let g1, g2 be continuous Function of P,P; ::_thesis: ( g1 <= g2 implies least_fix_point g1 <= least_fix_point g2 ) assume A1: g1 <= g2 ; ::_thesis: least_fix_point g1 <= least_fix_point g2 set p1 = sup (iter_min g1); set p2 = sup (iter_min g2); ( sup (iter_min g1) = least_fix_point g1 & sup (iter_min g2) = least_fix_point g2 ) by Th9; hence least_fix_point g1 <= least_fix_point g2 by A1, Th5; ::_thesis: verum end; begin 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 set IT = { 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 } ; not { 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 empty proof set z = the Element of Q; reconsider f = P --> the Element of Q as continuous Function of P,Q by Th7; f is Element of Funcs ( the carrier of P, the carrier of Q) by FUNCT_2:8; then f in { 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 } ; hence not { 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 empty ; ::_thesis: verum end; hence { 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 ; ::_thesis: verum 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 } ; Lm15: for P, Q being non empty strict chain-complete Poset for f being Function of P,Q holds f <= f proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being Function of P,Q holds f <= f let f be Function of P,Q; ::_thesis: f <= f for p being Element of P holds f . p <= f . p ; hence f <= f by YELLOW_2:9; ::_thesis: verum end; 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for f, g, h being Function of P,Q st f <= g & g <= h holds f <= h let f, g, h be Function of P,Q; ::_thesis: ( f <= g & g <= h implies f <= h ) assume A1: ( f <= g & g <= h ) ; ::_thesis: f <= h for p being Element of P holds f . p <= h . p proof let p be Element of P; ::_thesis: f . p <= h . p for q, q2 being Element of Q st q = f . p & q2 = h . p holds q <= q2 proof let q, q2 be Element of Q; ::_thesis: ( q = f . p & q2 = h . p implies q <= q2 ) assume A2: ( q = f . p & q2 = h . p ) ; ::_thesis: q <= q2 set q1 = g . p; ( q <= g . p & g . p <= q2 ) by A2, A1, YELLOW_2:9; hence q <= q2 by ORDERS_2:3; ::_thesis: verum end; hence f . p <= h . p ; ::_thesis: verum end; hence f <= h by YELLOW_2:9; ::_thesis: verum end; 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for f, g being Function of P,Q st f <= g & g <= f holds f = g let f, g be Function of P,Q; ::_thesis: ( f <= g & g <= f implies f = g ) assume A1: ( f <= g & g <= f ) ; ::_thesis: f = g for x being set st x in the carrier of P holds f . x = g . x proof let x be set ; ::_thesis: ( x in the carrier of P implies f . x = g . x ) assume x in the carrier of P ; ::_thesis: f . x = g . x then reconsider p = x as Element of P ; set q1 = f . p; set q2 = g . p; A2: f . p <= g . p by A1, YELLOW_2:9; g . p <= f . p by A1, YELLOW_2:9; hence f . x = g . x by A2, ORDERS_2:2; ::_thesis: verum end; hence f = g by FUNCT_2:12; ::_thesis: verum 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 defpred S1[ set , set ] means ex f, g being Function of P,Q st ( \$1 = f & \$2 = g & f <= g ); set X = ConFuncs (P,Q); consider IT being Relation of (ConFuncs (P,Q)),(ConFuncs (P,Q)) such that A1: for x, y being set holds ( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & S1[x,y] ) ) from RELSET_1:sch_1(); take IT ; ::_thesis: 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 ) ) ) thus 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 ) ) ) by A1; ::_thesis: verum 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 set X = ConFuncs (P,Q); let Y1, Y2 be Relation of (ConFuncs (P,Q)); ::_thesis: ( ( for x, y being set holds ( [x,y] in Y1 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 Y2 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 ) ) ) ) implies Y1 = Y2 ) defpred S1[ set , set ] means ( \$1 in ConFuncs (P,Q) & \$2 in ConFuncs (P,Q) & ex f, g being Function of P,Q st ( \$1 = f & \$2 = g & f <= g ) ); ( ( for x, y being set holds ( ( [x,y] in Y1 implies S1[x,y] ) & ( S1[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds ( [x,y] in Y2 iff S1[x,y] ) ) ) ) implies Y1 = Y2 ) proof assume A2: for x, y being set holds ( ( [x,y] in Y1 implies S1[x,y] ) & ( S1[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds ( [x,y] in Y2 iff S1[x,y] ) ) ) ; ::_thesis: Y1 = Y2 then A3: for x1, y1 being Element of ConFuncs (P,Q) holds ( [x1,y1] in Y1 iff S1[x1,y1] ) ; A4: for x, y being Element of ConFuncs (P,Q) holds ( [x,y] in Y2 iff S1[x,y] ) by A2; thus Y1 = Y2 from RELSET_1:sch_4(A3, A4); ::_thesis: verum end; hence ( ( for x, y being set holds ( [x,y] in Y1 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 Y2 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 ) ) ) ) implies Y1 = Y2 ) ; ::_thesis: verum 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 ) ) ) ); Lm18: for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: field (ConRelat (P,Q)) c= ConFuncs (P,Q) (ConFuncs (P,Q)) \/ (ConFuncs (P,Q)) c= ConFuncs (P,Q) ; hence field (ConRelat (P,Q)) c= ConFuncs (P,Q) by RELSET_1:8; ::_thesis: verum end; Lm19: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q) set R = ConRelat (P,Q); for x being set st x in ConFuncs (P,Q) holds [x,x] in ConRelat (P,Q) proof let x be set ; ::_thesis: ( x in ConFuncs (P,Q) implies [x,x] in ConRelat (P,Q) ) assume A1: x in ConFuncs (P,Q) ; ::_thesis: [x,x] in ConRelat (P,Q) then consider x1 being Element of Funcs ( the carrier of P, the carrier of Q) such that A2: x = x1 and A3: ex f being continuous Function of P,Q st f = x1 ; consider f being continuous Function of P,Q such that A4: f = x1 by A3; f <= f by Lm15; hence [x,x] in ConRelat (P,Q) by A1, A2, A4, Def7; ::_thesis: verum end; hence ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q) by RELAT_2:def_1; ::_thesis: verum end; Lm20: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) set X = ConFuncs (P,Q); set R = ConRelat (P,Q); for x, y, z being set st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) holds [x,z] in ConRelat (P,Q) proof let x, y, z be set ; ::_thesis: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) implies [x,z] in ConRelat (P,Q) ) assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) ) ; ::_thesis: [x,z] in ConRelat (P,Q) then consider f, g being Function of P,Q such that A2: ( x = f & y = g & f <= g ) by Def7; consider g1, h being Function of P,Q such that A3: ( y = g1 & z = h & g1 <= h ) by A1, Def7; f <= h by A3, A2, Lm16; hence [x,z] in ConRelat (P,Q) by A1, A2, A3, Def7; ::_thesis: verum end; hence ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) by RELAT_2:def_8; ::_thesis: verum end; Lm21: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q) set X = ConFuncs (P,Q); reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ; for x, y being set st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R holds x = y proof let x, y be set ; ::_thesis: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R implies x = y ) assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R ) ; ::_thesis: x = y then consider f, g being Function of P,Q such that A2: ( x = f & y = g & f <= g ) by Def7; consider g1, f1 being Function of P,Q such that A3: ( y = g1 & x = f1 & g1 <= f1 ) by A1, Def7; thus x = y by A2, A3, Lm17; ::_thesis: verum end; hence ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q) by RELAT_2:def_4; ::_thesis: verum end; registration let P, Q be non empty strict chain-complete Poset; cluster ConRelat (P,Q) -> reflexive ; coherence ConRelat (P,Q) is reflexive proof ConRelat (P,Q) is_reflexive_in field (ConRelat (P,Q)) proof reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ; for x being set st x in field R holds [x,x] in R proof let x be set ; ::_thesis: ( x in field R implies [x,x] in R ) assume A1: x in field R ; ::_thesis: [x,x] in R A2: field R c= ConFuncs (P,Q) by Lm18; R is_reflexive_in ConFuncs (P,Q) by Lm19; hence [x,x] in R by A1, A2, RELAT_2:def_1; ::_thesis: verum end; hence ConRelat (P,Q) is_reflexive_in field (ConRelat (P,Q)) by RELAT_2:def_1; ::_thesis: verum end; hence ConRelat (P,Q) is reflexive by RELAT_2:def_9; ::_thesis: verum end; cluster ConRelat (P,Q) -> transitive ; coherence ConRelat (P,Q) is transitive proof ConRelat (P,Q) is_transitive_in field (ConRelat (P,Q)) proof set X = field (ConRelat (P,Q)); set R = ConRelat (P,Q); for x, y, z being set st x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) holds [x,z] in ConRelat (P,Q) proof let x, y, z be set ; ::_thesis: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) implies [x,z] in ConRelat (P,Q) ) assume A3: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) ) ; ::_thesis: [x,z] in ConRelat (P,Q) set X1 = ConFuncs (P,Q); A4: field (ConRelat (P,Q)) c= ConFuncs (P,Q) by Lm18; ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) by Lm20; hence [x,z] in ConRelat (P,Q) by A3, A4, RELAT_2:def_8; ::_thesis: verum end; hence ConRelat (P,Q) is_transitive_in field (ConRelat (P,Q)) by RELAT_2:def_8; ::_thesis: verum end; hence ConRelat (P,Q) is transitive by RELAT_2:def_16; ::_thesis: verum end; cluster ConRelat (P,Q) -> antisymmetric ; coherence ConRelat (P,Q) is antisymmetric proof ConRelat (P,Q) is_antisymmetric_in field (ConRelat (P,Q)) proof set X = field (ConRelat (P,Q)); reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ; for x, y being set st x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R holds x = y proof let x, y be set ; ::_thesis: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R implies x = y ) assume A5: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R ) ; ::_thesis: x = y set X1 = ConFuncs (P,Q); A6: field R c= ConFuncs (P,Q) by Lm18; R is_antisymmetric_in ConFuncs (P,Q) by Lm21; hence x = y by A5, A6, RELAT_2:def_4; ::_thesis: verum end; hence ConRelat (P,Q) is_antisymmetric_in field (ConRelat (P,Q)) by RELAT_2:def_4; ::_thesis: verum end; hence ConRelat (P,Q) is antisymmetric by RELAT_2:def_12; ::_thesis: verum 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; proof set IT = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #); A1: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_reflexive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm19; A2: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_transitive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm20; the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_antisymmetric_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm21; hence RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset by A1, A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum end; 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; proof set R = the InternalRel of Q; set IT = { x where x is Element of Q : ex f being continuous Function of P,Q st ( f in F & x = f . p ) } ; for x being set st x in { x where x is Element of Q : ex f being continuous Function of P,Q st ( f in F & x = f . p ) } holds x in the carrier of Q proof let x be set ; ::_thesis: ( x in { x where x is Element of Q : ex f being continuous Function of P,Q st ( f in F & x = f . p ) } implies x in the carrier of Q ) assume x in { x where x is Element of Q : ex f being continuous Function of P,Q st ( f in F & x = f . p ) } ; ::_thesis: x in the carrier of Q then consider a being Element of Q such that A1: ( x = a & ex f being continuous Function of P,Q st ( f in F & a = f . p ) ) ; reconsider x = x as Element of the carrier of Q by A1; x in the carrier of Q ; hence x in the carrier of Q ; ::_thesis: verum end; then reconsider IT = { x where x is Element of Q : ex f being continuous Function of P,Q st ( f in F & x = f . p ) } as Subset of Q by TARSKI:def_3; for x, y being set st x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q holds [y,x] in the InternalRel of Q proof let x, y be set ; ::_thesis: ( x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q implies [y,x] in the InternalRel of Q ) assume A2: ( x in IT & y in IT & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) then consider a being Element of Q such that A3: ( x = a & ex f being continuous Function of P,Q st ( f in F & a = f . p ) ) ; consider f being continuous Function of P,Q such that A4: ( f in F & a = f . p ) by A3; consider b being Element of Q such that A5: ( y = b & ex g being continuous Function of P,Q st ( g in F & b = g . p ) ) by A2; consider g being continuous Function of P,Q such that A6: ( g in F & b = g . p ) by A5; set S = the InternalRel of (ConPoset (P,Q)); A7: the InternalRel of (ConPoset (P,Q)) is_strongly_connected_in F by ORDERS_2:def_7; percases ( [f,g] in the InternalRel of (ConPoset (P,Q)) or [g,f] in the InternalRel of (ConPoset (P,Q)) ) by A7, A4, A6, RELAT_2:def_7; suppose [f,g] in the InternalRel of (ConPoset (P,Q)) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) then consider f1, g1 being Function of P,Q such that A8: ( f = f1 & g = g1 & f1 <= g1 ) by Def7; a <= b by A8, A4, A6, YELLOW_2:9; hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def_5; ::_thesis: verum end; suppose [g,f] in the InternalRel of (ConPoset (P,Q)) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) then consider g1, f1 being Function of P,Q such that A9: ( g = g1 & f = f1 & g1 <= f1 ) by Def7; b <= a by A9, A4, A6, YELLOW_2:9; hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def_5; ::_thesis: verum end; end; end; then A10: the InternalRel of Q is_connected_in IT by RELAT_2:def_6; for x being set st x in IT holds [x,x] in the InternalRel of Q proof let x be set ; ::_thesis: ( x in IT implies [x,x] in the InternalRel of Q ) assume x in IT ; ::_thesis: [x,x] in the InternalRel of Q then reconsider x = x as Element of Q ; x <= x ; hence [x,x] in the InternalRel of Q by ORDERS_2:def_5; ::_thesis: verum end; then the InternalRel of Q is_reflexive_in IT by RELAT_2:def_1; then the InternalRel of Q is_strongly_connected_in IT by A10, ORDERS_1:7; then reconsider IT = IT as Chain of Q by ORDERS_2:def_7; consider a being set such that A11: a in F by XBOOLE_0:7; a in ConFuncs (P,Q) by A11; then consider b being Element of Funcs ( the carrier of P, the carrier of Q) such that A12: ( a = b & ex f being continuous Function of P,Q st f = b ) ; consider f being continuous Function of P,Q such that A13: f = b by A12; reconsider c = f . p as Element of Q ; c in IT by A11, A12, A13; hence { 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 ; ::_thesis: verum 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 set X = the carrier of P; set Y = the carrier of Q; defpred S1[ set , set ] means for p being Element of P for M being non empty Chain of Q st p = \$1 & M = F -image p holds \$2 = sup M; A1: for x being set st x in the carrier of P holds ex y being set st ( y in the carrier of Q & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier of P implies ex y being set st ( y in the carrier of Q & S1[x,y] ) ) assume x in the carrier of P ; ::_thesis: ex y being set st ( y in the carrier of Q & S1[x,y] ) then reconsider x = x as Element of P ; reconsider a = F -image x as non empty Chain of Q ; set y = sup a; take sup a ; ::_thesis: ( sup a in the carrier of Q & S1[x, sup a] ) thus ( sup a in the carrier of Q & S1[x, sup a] ) ; ::_thesis: verum end; consider IT being Function of the carrier of P, the carrier of Q such that A2: for x being set st x in the carrier of P holds S1[x,IT . x] from FUNCT_2:sch_1(A1); for p being Element of P for M being non empty Chain of Q st M = F -image p holds IT . p = sup M by A2; hence 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 ; ::_thesis: verum 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 let f, g be Function of P,Q; ::_thesis: ( ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds f . p = sup M ) & ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds g . p = sup M ) implies f = g ) ( ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds f . p = sup M ) & ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds g . p = sup M ) implies f = g ) proof assume A3: ( ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds f . p = sup M ) & ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds g . p = sup M ) ) ; ::_thesis: f = g set X = the carrier of P; for x being set st x in the carrier of P holds f . x = g . x proof let x be set ; ::_thesis: ( x in the carrier of P implies f . x = g . x ) assume x in the carrier of P ; ::_thesis: f . x = g . x then reconsider p = x as Element of P ; reconsider M = F -image p as non empty Chain of Q ; f . x = sup M by A3 .= g . x by A3 ; hence f . x = g . x ; ::_thesis: verum end; hence f = g by FUNCT_2:12; ::_thesis: verum end; hence ( ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds f . p = sup M ) & ( for p being Element of P for M being non empty Chain of Q st M = F -image p holds g . p = sup M ) implies f = g ) ; ::_thesis: verum 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 ); 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is monotone let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is monotone reconsider f = sup_func F as Function of P,Q ; for p, p1 being Element of P st p <= p1 holds for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds q <= q1 proof let p, p1 be Element of P; ::_thesis: ( p <= p1 implies for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds q <= q1 ) assume A1: p <= p1 ; ::_thesis: for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds q <= q1 for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds q <= q1 proof let q, q1 be Element of Q; ::_thesis: ( q = f . p & q1 = f . p1 implies q <= q1 ) assume A2: ( q = f . p & q1 = f . p1 ) ; ::_thesis: q <= q1 reconsider X = F -image p as non empty Chain of Q ; reconsider X1 = F -image p1 as non empty Chain of Q ; A3: ( ex_sup_of X,Q & ex_sup_of X1,Q ) by Def1; A4: q = sup X by A2, Def10; q1 = sup X1 by A2, Def10; then A5: X1 is_<=_than q1 by A3, YELLOW_0:def_9; for x being Element of Q st x in X holds x <= q1 proof let x be Element of Q; ::_thesis: ( x in X implies x <= q1 ) assume x in X ; ::_thesis: x <= q1 then consider a being Element of Q such that A6: ( x = a & ex g being continuous Function of P,Q st ( g in F & a = g . p ) ) ; consider g being continuous Function of P,Q such that A7: ( g in F & a = g . p ) by A6; reconsider b = g . p1 as Element of Q ; A8: a <= b by A1, A7, ORDERS_3:def_5; b in X1 by A7; then b <= q1 by A5, LATTICE3:def_9; hence x <= q1 by A6, A8, ORDERS_2:3; ::_thesis: verum end; then X is_<=_than q1 by LATTICE3:def_9; hence q <= q1 by A3, A4, YELLOW_0:def_9; ::_thesis: verum end; hence for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds q <= q1 ; ::_thesis: verum end; hence sup_func F is monotone by ORDERS_3:def_5; ::_thesis: verum end; 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 proof let Q be non empty strict chain-complete Poset; ::_thesis: for M being non empty Chain of Q for q being Element of Q st q in M holds q <= sup M let M be non empty Chain of Q; ::_thesis: for q being Element of Q st q in M holds q <= sup M let q be Element of Q; ::_thesis: ( q in M implies q <= sup M ) assume A1: q in M ; ::_thesis: q <= sup M A2: ex_sup_of M,Q by Def1; set x = sup M; M is_<=_than sup M by A2, YELLOW_0:def_9; hence q <= sup M by A1, LATTICE3:def_9; ::_thesis: verum end; 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 proof let Q be non empty strict chain-complete Poset; ::_thesis: 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 let M be non empty Chain of Q; ::_thesis: for q1 being Element of Q st ( for q being Element of Q st q in M holds q <= q1 ) holds sup M <= q1 let q1 be Element of Q; ::_thesis: ( ( for q being Element of Q st q in M holds q <= q1 ) implies sup M <= q1 ) assume for q being Element of Q st q in M holds q <= q1 ; ::_thesis: sup M <= q1 then A1: M is_<=_than q1 by LATTICE3:def_9; A2: ex_sup_of M,Q by Def1; thus sup M <= q1 by A2, A1, YELLOW_0:def_9; ::_thesis: verum end; 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is continuous reconsider f = sup_func F as monotone Function of P,Q by Lm22; for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) proof let L be non empty Chain of P; ::_thesis: f . (sup L) <= sup (f .: L) reconsider M1 = f .: L as non empty Chain of Q by Th1; set q1 = sup M1; set a = sup L; set M = F -image (sup L); A1: f . (sup L) = sup (F -image (sup L)) by Def10; for q being Element of Q st q in F -image (sup L) holds q <= sup M1 proof let q be Element of Q; ::_thesis: ( q in F -image (sup L) implies q <= sup M1 ) assume q in F -image (sup L) ; ::_thesis: q <= sup M1 then consider q0 being Element of Q such that A2: ( q = q0 & ex g being continuous Function of P,Q st ( g in F & q0 = g . (sup L) ) ) ; consider g being continuous Function of P,Q such that A3: ( g in F & q0 = g . (sup L) ) by A2; reconsider M2 = g .: L as non empty Chain of Q by Th1; A4: q = sup M2 by Th6, A2, A3; for q2 being Element of Q st q2 in M2 holds q2 <= sup M1 proof let q2 be Element of Q; ::_thesis: ( q2 in M2 implies q2 <= sup M1 ) assume q2 in M2 ; ::_thesis: q2 <= sup M1 then consider x being set such that A5: ( x in dom g & x in L & q2 = g . x ) by FUNCT_1:def_6; reconsider x = x as Element of P by A5; set Mx = F -image x; A6: f . x = sup (F -image x) by Def10; set y = f . x; x in the carrier of P ; then x in dom f by FUNCT_2:def_1; then f . x in M1 by A5, FUNCT_1:def_6; then A7: f . x <= sup M1 by Lm23; q2 in F -image x by A5, A3; then q2 <= sup (F -image x) by Lm23; hence q2 <= sup M1 by A7, A6, ORDERS_2:3; ::_thesis: verum end; hence q <= sup M1 by A4, Lm24; ::_thesis: verum end; hence f . (sup L) <= sup (f .: L) by A1, Lm24; ::_thesis: verum end; hence sup_func F is continuous by Th8; ::_thesis: verum 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 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)) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is Element of (ConPoset (P,Q)) let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is Element of (ConPoset (P,Q)) set x = sup_func F; A1: sup_func F is Element of Funcs ( the carrier of P, the carrier of Q) by FUNCT_2:8; reconsider x = sup_func F as continuous Function of P,Q ; x in ConFuncs (P,Q) by A1; hence sup_func F is Element of (ConPoset (P,Q)) ; ::_thesis: verum end; 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 proof let P, Q be non empty strict chain-complete Poset; ::_thesis: 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 let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: for x being set st x in F holds ex g being continuous Function of P,Q st x = g let x be set ; ::_thesis: ( x in F implies ex g being continuous Function of P,Q st x = g ) assume x in F ; ::_thesis: ex g being continuous Function of P,Q st x = g then x in ConFuncs (P,Q) ; then consider y being Element of Funcs ( the carrier of P, the carrier of Q) such that A1: ( x = y & ex g being continuous Function of P,Q st g = y ) ; thus ex g being continuous Function of P,Q st x = g by A1; ::_thesis: verum 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 let P, Q be non empty strict chain-complete Poset; ::_thesis: 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))) ) let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) ) set X = ConPoset (P,Q); set f1 = sup_func F; reconsider f = sup_func F as Element of (ConPoset (P,Q)) by Lm26; for x being Element of (ConPoset (P,Q)) st x in F holds x <= f proof let x be Element of (ConPoset (P,Q)); ::_thesis: ( x in F implies x <= f ) assume A1: x in F ; ::_thesis: x <= f then consider g1 being continuous Function of P,Q such that A2: x = g1 by Lm27; reconsider g = g1 as Element of (ConPoset (P,Q)) by A2; for p being Element of P holds g1 . p <= (sup_func F) . p proof let p be Element of P; ::_thesis: g1 . p <= (sup_func F) . p for q1, q2 being Element of Q st q1 = g1 . p & q2 = (sup_func F) . p holds q1 <= q2 proof let q1, q2 be Element of Q; ::_thesis: ( q1 = g1 . p & q2 = (sup_func F) . p implies q1 <= q2 ) assume A3: ( q1 = g1 . p & q2 = (sup_func F) . p ) ; ::_thesis: q1 <= q2 then A4: q1 in F -image p by A1, A2; reconsider M = F -image p as non empty Chain of Q ; q2 = sup M by Def10, A3; hence q1 <= q2 by A4, Lm23; ::_thesis: verum end; hence g1 . p <= (sup_func F) . p ; ::_thesis: verum end; then g1 <= sup_func F by YELLOW_2:9; then [g,f] in ConRelat (P,Q) by Def7; hence x <= f by A2, ORDERS_2:def_5; ::_thesis: verum end; then A5: F is_<=_than f by LATTICE3:def_9; for y being Element of (ConPoset (P,Q)) st F is_<=_than y holds f <= y proof let y be Element of (ConPoset (P,Q)); ::_thesis: ( F is_<=_than y implies f <= y ) y in ConFuncs (P,Q) ; then consider y1 being Element of Funcs ( the carrier of P, the carrier of Q) such that A6: ( y = y1 & ex gy being continuous Function of P,Q st gy = y1 ) ; consider gy being continuous Function of P,Q such that A7: gy = y1 by A6; ( F is_<=_than y implies f <= y ) proof assume A8: F is_<=_than y ; ::_thesis: f <= y for p being Element of P holds (sup_func F) . p <= gy . p proof let p be Element of P; ::_thesis: (sup_func F) . p <= gy . p for q1, q2 being Element of Q st q1 = (sup_func F) . p & q2 = gy . p holds q1 <= q2 proof let q1, q2 be Element of Q; ::_thesis: ( q1 = (sup_func F) . p & q2 = gy . p implies q1 <= q2 ) assume A9: ( q1 = (sup_func F) . p & q2 = gy . p ) ; ::_thesis: q1 <= q2 reconsider M = F -image p as non empty Chain of Q ; for q being Element of Q st q in M holds q <= q2 proof let q be Element of Q; ::_thesis: ( q in M implies q <= q2 ) assume q in M ; ::_thesis: q <= q2 then consider a being Element of Q such that A10: ( q = a & ex g being continuous Function of P,Q st ( g in F & a = g . p ) ) ; consider g being continuous Function of P,Q such that A11: ( g in F & a = g . p ) by A10; reconsider g1 = g as Element of (ConPoset (P,Q)) by A11; g1 <= y by A8, A11, LATTICE3:def_9; then [g1,y] in ConRelat (P,Q) by ORDERS_2:def_5; then consider g2, g3 being Function of P,Q such that A12: ( g1 = g2 & y = g3 & g2 <= g3 ) by Def7; thus q <= q2 by A12, A6, A7, A10, A11, A9, YELLOW_2:9; ::_thesis: verum end; then sup M <= q2 by Lm24; hence q1 <= q2 by A9, Def10; ::_thesis: verum end; hence (sup_func F) . p <= gy . p ; ::_thesis: verum end; then sup_func F <= gy by YELLOW_2:9; then [f,y] in ConRelat (P,Q) by A6, A7, Def7; hence f <= y by ORDERS_2:def_5; ::_thesis: verum end; hence ( F is_<=_than y implies f <= y ) ; ::_thesis: verum end; hence ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) ) by A5, YELLOW_0:30; ::_thesis: verum 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; Lm28: for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q)) proof let P, Q be non empty strict chain-complete Poset; ::_thesis: min_func (P,Q) is Element of (ConPoset (P,Q)) reconsider f = min_func (P,Q) as continuous Function of P,Q ; reconsider x = f as Element of Funcs ( the carrier of P, the carrier of Q) by FUNCT_2:8; x in ConFuncs (P,Q) ; hence min_func (P,Q) is Element of (ConPoset (P,Q)) ; ::_thesis: verum 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 let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds f is_<=_than the carrier of (ConPoset (P,Q)) let f be Element of (ConPoset (P,Q)); ::_thesis: ( f = min_func (P,Q) implies f is_<=_than the carrier of (ConPoset (P,Q)) ) assume A1: f = min_func (P,Q) ; ::_thesis: f is_<=_than the carrier of (ConPoset (P,Q)) set f1 = min_func (P,Q); for x being Element of (ConPoset (P,Q)) holds f <= x proof let x be Element of (ConPoset (P,Q)); ::_thesis: f <= x x in ConFuncs (P,Q) ; then consider x1 being Element of Funcs ( the carrier of P, the carrier of Q) such that A2: ( x = x1 & ex g being continuous Function of P,Q st g = x1 ) ; consider g being continuous Function of P,Q such that A3: g = x1 by A2; for p being Element of P holds (min_func (P,Q)) . p <= g . p proof let p be Element of P; ::_thesis: (min_func (P,Q)) . p <= g . p for q1, q2 being Element of Q st q1 = (min_func (P,Q)) . p & q2 = g . p holds q1 <= q2 proof let q1, q2 be Element of Q; ::_thesis: ( q1 = (min_func (P,Q)) . p & q2 = g . p implies q1 <= q2 ) assume ( q1 = (min_func (P,Q)) . p & q2 = g . p ) ; ::_thesis: q1 <= q2 then q1 = Bottom Q by FUNCOP_1:7; hence q1 <= q2 by YELLOW_0:44; ::_thesis: verum end; hence (min_func (P,Q)) . p <= g . p ; ::_thesis: verum end; then min_func (P,Q) <= g by YELLOW_2:9; then [f,x] in ConRelat (P,Q) by A2, A3, Def7, A1; hence f <= x by ORDERS_2:def_5; ::_thesis: verum end; hence f is_<=_than the carrier of (ConPoset (P,Q)) by Lm4; ::_thesis: verum 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 set IT = ConPoset (P,Q); ex a being Element of (ConPoset (P,Q)) st a is_<=_than the carrier of (ConPoset (P,Q)) proof reconsider a = min_func (P,Q) as Element of (ConPoset (P,Q)) by Lm28; take a ; ::_thesis: a is_<=_than the carrier of (ConPoset (P,Q)) thus a is_<=_than the carrier of (ConPoset (P,Q)) by Th12; ::_thesis: verum end; then A1: ConPoset (P,Q) is lower-bounded by YELLOW_0:def_4; for L being Chain of (ConPoset (P,Q)) st not L is empty holds ex_sup_of L, ConPoset (P,Q) by Th11; hence ConPoset (P,Q) is chain-complete by Def1, A1; ::_thesis: verum end; 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 proof let x be set ; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: ( x is Element of (ConPoset (P,P)) implies x is continuous Function of P,P ) assume x is Element of (ConPoset (P,P)) ; ::_thesis: x is continuous Function of P,P then x in ConFuncs (P,P) ; then consider y being Element of Funcs ( the carrier of P, the carrier of P) such that A1: ( x = y & ex g being continuous Function of P,P st g = y ) ; thus x is continuous Function of P,P by A1; ::_thesis: verum end; 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)) proof let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P st g is continuous Function of P,P holds g is Element of (ConPoset (P,P)) let g be monotone Function of P,P; ::_thesis: ( g is continuous Function of P,P implies g is Element of (ConPoset (P,P)) ) assume A1: g is continuous Function of P,P ; ::_thesis: g is Element of (ConPoset (P,P)) reconsider g1 = g as Element of Funcs ( the carrier of P, the carrier of P) by FUNCT_2:8; g1 in ConFuncs (P,P) by A1; hence g is Element of (ConPoset (P,P)) ; ::_thesis: verum 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 set X = the carrier of (ConPoset (P,P)); set Y = the carrier of P; defpred S1[ set , set ] means for g being Element of (ConPoset (P,P)) for h being continuous Function of P,P st g = h & g = \$1 holds \$2 = least_fix_point h; A1: for x being set st x in the carrier of (ConPoset (P,P)) holds ex y being set st ( y in the carrier of P & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier of (ConPoset (P,P)) implies ex y being set st ( y in the carrier of P & S1[x,y] ) ) assume x in the carrier of (ConPoset (P,P)) ; ::_thesis: ex y being set st ( y in the carrier of P & S1[x,y] ) then reconsider x = x as Element of (ConPoset (P,P)) ; reconsider h = x as continuous Function of P,P by Lm29; take least_fix_point h ; ::_thesis: ( least_fix_point h in the carrier of P & S1[x, least_fix_point h] ) thus ( least_fix_point h in the carrier of P & S1[x, least_fix_point h] ) ; ::_thesis: verum end; consider IT being Function of the carrier of (ConPoset (P,P)), the carrier of P such that A2: for x being set st x in the carrier of (ConPoset (P,P)) holds S1[x,IT . x] from FUNCT_2:sch_1(A1); 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 by A2; hence 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 ; ::_thesis: verum 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 let h1, h2 be Function of (ConPoset (P,P)),P; ::_thesis: ( ( for g being Element of (ConPoset (P,P)) for h being continuous Function of P,P st g = h holds h1 . 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 h2 . g = least_fix_point h ) implies h1 = h2 ) assume A3: ( ( for g being Element of (ConPoset (P,P)) for h being continuous Function of P,P st g = h holds h1 . 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 h2 . g = least_fix_point h ) ) ; ::_thesis: h1 = h2 set X = the carrier of (ConPoset (P,P)); for x being set st x in the carrier of (ConPoset (P,P)) holds h1 . x = h2 . x proof let x be set ; ::_thesis: ( x in the carrier of (ConPoset (P,P)) implies h1 . x = h2 . x ) assume x in the carrier of (ConPoset (P,P)) ; ::_thesis: h1 . x = h2 . x then reconsider g = x as Element of (ConPoset (P,P)) ; reconsider h = g as continuous Function of P,P by Lm29; h1 . x = least_fix_point h by A3 .= h2 . x by A3 ; hence h1 . x = h2 . x ; ::_thesis: verum end; hence h1 = h2 by FUNCT_2:12; ::_thesis: verum 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 ); 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 ) ) proof let P be non empty strict chain-complete Poset; ::_thesis: 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 ) ) let p1, p2 be Element of (ConPoset (P,P)); ::_thesis: ( p1 <= p2 implies ( 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 ) ) ) assume p1 <= p2 ; ::_thesis: ( 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 ) ) then A1: [p1,p2] in ConRelat (P,P) by ORDERS_2:def_5; ex g1, g2 being continuous Function of P,P st ( p1 = g1 & p2 = g2 & g1 <= g2 ) proof consider g1, g2 being Function of P,P such that A2: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, Def7; reconsider h1 = p1, h2 = p2 as continuous Function of P,P by Lm29; g1 = h1 by A2; then reconsider g1 = g1 as continuous Function of P,P ; g2 = h2 by A2; then reconsider g2 = g2 as continuous Function of P,P ; take g1 ; ::_thesis: ex g2 being continuous Function of P,P st ( p1 = g1 & p2 = g2 & g1 <= g2 ) take g2 ; ::_thesis: ( p1 = g1 & p2 = g2 & g1 <= g2 ) thus ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A2; ::_thesis: verum end; hence ( 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 ) ) ; ::_thesis: verum end; Lm32: for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P proof let P be non empty strict chain-complete Poset; ::_thesis: fix_func P is monotone Function of (ConPoset (P,P)),P set IT = fix_func P; for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds a <= b proof let p1, p2 be Element of (ConPoset (P,P)); ::_thesis: ( p1 <= p2 implies for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds a <= b ) assume A1: p1 <= p2 ; ::_thesis: for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds a <= b let a, b be Element of P; ::_thesis: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 implies a <= b ) assume A2: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 ) ; ::_thesis: a <= b consider g1, g2 being continuous Function of P,P such that A3: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, Lm31; ( a = least_fix_point g1 & b = least_fix_point g2 ) by A2, Def12, A3; hence a <= b by A3, Th10; ::_thesis: verum end; hence fix_func P is monotone Function of (ConPoset (P,P)),P by ORDERS_3:def_5; ::_thesis: verum end; 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) ) proof let P be non empty strict chain-complete Poset; ::_thesis: 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) ) let G be non empty Chain of (ConPoset (P,P)); ::_thesis: 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) ) let n be Nat; ::_thesis: 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) ) let X, x be set ; ::_thesis: ( 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 implies 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) ) ) assume ( 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 ) ; ::_thesis: 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) ) then consider p being Element of P such that A1: ( x = 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) ) ) ; thus 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) ) by A1; ::_thesis: verum end; 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 proof let x be set ; ::_thesis: 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 let P be non empty strict chain-complete Poset; ::_thesis: 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 let G be non empty Chain of (ConPoset (P,P)); ::_thesis: 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 let n be Nat; ::_thesis: 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 let X be set ; ::_thesis: ( 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 implies x is Element of P ) assume A1: 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) ) } ; ::_thesis: ( not x in X or x is Element of P ) ( x in X implies x is Element of P ) proof assume x in X ; ::_thesis: x is Element of P then consider p being Element of P such that A2: ( x = 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) ) ) by A1; thus x is Element of P by A2; ::_thesis: verum end; hence ( not x in X or x is Element of P ) ; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let G be non empty Chain of (ConPoset (P,P)); ::_thesis: 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 let n be Nat; ::_thesis: 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 let X be set ; ::_thesis: ( 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) ) } implies X is non empty Subset of P ) assume A1: 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) ) } ; ::_thesis: X is non empty Subset of P consider g being set such that A2: g in G by XBOOLE_0:def_1; reconsider g = g as Element of (ConPoset (P,P)) by A2; reconsider gg = g as continuous Function of P,P by Lm29; reconsider p = (iter (gg,n)) . (Bottom P) as Element of P by Lm6; A3: p in X by A1, A2; for x being set st x in X holds x in the carrier of P proof let x be set ; ::_thesis: ( x in X implies x in the carrier of P ) assume x in X ; ::_thesis: x in the carrier of P then x is Element of the carrier of P by Lm34, A1; hence x in the carrier of P ; ::_thesis: verum end; hence X is non empty Subset of P by A3, TARSKI:def_3; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds g <= f let f, g be monotone Function of P,P; ::_thesis: ( f in G & g in G & not f <= g implies g <= f ) assume A1: ( f in G & g in G ) ; ::_thesis: ( f <= g or g <= f ) set S = the InternalRel of (ConPoset (P,P)); A2: the InternalRel of (ConPoset (P,P)) is_strongly_connected_in G by ORDERS_2:def_7; percases ( [f,g] in the InternalRel of (ConPoset (P,P)) or [g,f] in the InternalRel of (ConPoset (P,P)) ) by A2, A1, RELAT_2:def_7; suppose [f,g] in the InternalRel of (ConPoset (P,P)) ; ::_thesis: ( f <= g or g <= f ) then consider f1, g1 being Function of P,P such that A3: ( f = f1 & g = g1 & f1 <= g1 ) by Def7; thus ( f <= g or g <= f ) by A3; ::_thesis: verum end; suppose [g,f] in the InternalRel of (ConPoset (P,P)) ; ::_thesis: ( f <= g or g <= f ) then consider g1, f1 being Function of P,P such that A4: ( g = g1 & f = f1 & g1 <= f1 ) by Def7; thus ( f <= g or g <= f ) by A4; ::_thesis: verum end; end; end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let G be non empty Chain of (ConPoset (P,P)); ::_thesis: 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 let n be Nat; ::_thesis: 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 let X be set ; ::_thesis: ( 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) ) } implies X is non empty Chain of P ) assume A1: 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) ) } ; ::_thesis: X is non empty Chain of P set R = the InternalRel of P; reconsider X = X as non empty Subset of P by A1, Lm35; for x, y being set st x in X & y in X & x <> y & not [x,y] in the InternalRel of P holds [y,x] in the InternalRel of P proof let x, y be set ; ::_thesis: ( x in X & y in X & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P ) assume A2: ( x in X & y in X & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) then consider p1 being Element of P, g1 being continuous Function of P,P such that A3: ( x = p1 & g1 in G & p1 = (iter (g1,n)) . (Bottom P) ) by A1, Lm33; consider p2 being Element of P, g2 being continuous Function of P,P such that A4: ( y = p2 & g2 in G & p2 = (iter (g2,n)) . (Bottom P) ) by A1, A2, Lm33; percases ( g1 <= g2 or g2 <= g1 ) by A3, A4, Lm36; suppose g1 <= g2 ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) then p1 <= p2 by Lm12, A3, A4; hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def_5; ::_thesis: verum end; suppose g2 <= g1 ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) then p2 <= p1 by Lm12, A3, A4; hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def_5; ::_thesis: verum end; end; end; then A5: the InternalRel of P is_connected_in X by RELAT_2:def_6; for x being set st x in X holds [x,x] in the InternalRel of P proof let x be set ; ::_thesis: ( x in X implies [x,x] in the InternalRel of P ) assume x in X ; ::_thesis: [x,x] in the InternalRel of P then reconsider x = x as Element of P ; x <= x ; hence [x,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum end; then the InternalRel of P is_reflexive_in X by RELAT_2:def_1; then the InternalRel of P is_strongly_connected_in X by A5, ORDERS_1:7; hence X is non empty Chain of P by ORDERS_2:def_7; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let h be Function of (ConPoset (P,P)),P; ::_thesis: for G being non empty Chain of (ConPoset (P,P)) for x being set st x in G holds h . x in h .: G let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for x being set st x in G holds h . x in h .: G let x be set ; ::_thesis: ( x in G implies h . x in h .: G ) assume A1: x in G ; ::_thesis: h . x in h .: G set X = the carrier of (ConPoset (P,P)); set Y = the carrier of P; reconsider h = h as Function of the carrier of (ConPoset (P,P)), the carrier of P ; x in the carrier of (ConPoset (P,P)) by A1; then x in dom h by FUNCT_2:def_1; hence h . x in h .: G by A1, FUNCT_1:def_6; ::_thesis: verum end; 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 proof let P be non empty strict chain-complete Poset; ::_thesis: 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 let g be continuous Function of P,P; ::_thesis: 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 let p, p1 be Element of P; ::_thesis: for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds p1 <= p let n be Nat; ::_thesis: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) implies p1 <= p ) set a = Bottom P; assume A1: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) ) ; ::_thesis: p1 <= p then A2: p1 in iterSet (g,(Bottom P)) ; reconsider g1 = g as Element of (ConPoset (P,P)) by Lm30; reconsider G1 = g1 as continuous Function of P,P ; p = least_fix_point G1 by Def12, A1 .= sup (iter_min g) by Th9 ; hence p1 <= p by Lm23, A2; ::_thesis: verum end; 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)) ) proof let P be non empty strict chain-complete Poset; ::_thesis: 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)) ) let G be non empty Chain of (ConPoset (P,P)); ::_thesis: 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)) ) let x be set ; ::_thesis: 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)) ) let n be Nat; ::_thesis: 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)) ) let M be non empty Chain of P; ::_thesis: 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)) ) let g1 be monotone Function of P,P; ::_thesis: ( 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 implies ex g being continuous Function of P,P st ( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) ) ) assume A1: ( 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 ) ; ::_thesis: ex g being continuous Function of P,P st ( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) ) then ex y being set st ( y in dom g1 & y in M & x = g1 . y ) by FUNCT_1:def_6; then consider y being Element of M such that A2: ( y in M & x = g1 . y ) ; consider p being Element of P such that A3: ( y = 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) ) ) by A1, A2; thus ex g being continuous Function of P,P st ( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) ) by A2, A3; ::_thesis: verum end; 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) proof let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G) let G be non empty Chain of (ConPoset (P,P)); ::_thesis: (fix_func P) . (sup G) <= sup ((fix_func P) .: G) reconsider h = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm32; h . (sup G) <= sup (h .: G) proof reconsider L = h .: G as non empty Chain of P by Th1; set g0 = sup G; set p0 = h . (sup G); reconsider G0 = sup G as continuous Function of P,P by Lm29; A1: h . (sup G) = least_fix_point G0 by Def12; A2: sup G = sup_func G by Th11; then reconsider g0 = sup G as continuous Function of P,P ; set a = Bottom P; reconsider I0 = iterSet (g0,(Bottom P)) as non empty Chain of P by Th3; A3: h . (sup G) = sup (iter_min g0) by Th9, A1 .= sup I0 ; A4: ex_sup_of I0,P by Def1; for x being Element of P st x in I0 holds x <= sup L proof let x be Element of P; ::_thesis: ( x in I0 implies x <= sup L ) assume x in I0 ; ::_thesis: x <= sup L then consider y being Element of P such that A5: ( x = y & ex n being Nat st y = (iter (g0,n)) . (Bottom P) ) ; consider n0 being Nat such that A6: x = (iter (g0,n0)) . (Bottom P) by A5; set M0 = { 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,n0)) . (Bottom P) ) } ; reconsider M0 = { 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,n0)) . (Bottom P) ) } as non empty Chain of P by Lm37; for p being Element of P st p in M0 holds p <= sup L proof let p be Element of P; ::_thesis: ( p in M0 implies p <= sup L ) assume p in M0 ; ::_thesis: p <= sup L then consider p0 being Element of P, g being continuous Function of P,P such that A7: ( p = p0 & g in G & p0 = (iter (g,n0)) . (Bottom P) ) by Lm33; set r = h . g; h . g in L by A7, Lm38; then reconsider r = h . g as Element of P ; A8: r <= sup L by Lm23, A7, Lm38; p <= r by A7, Lm39; hence p <= sup L by A8, ORDERS_2:3; ::_thesis: verum end; then A9: sup M0 <= sup L by Lm24; defpred S1[ Nat] means for z being Element of P for M being non empty Chain of P st z = (iter (g0,\$1)) . (Bottom P) & 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,\$1)) . (Bottom P) ) } holds z <= sup M; A10: S1[ 0 ] proof let z be Element of P; ::_thesis: for M being non empty Chain of P st z = (iter (g0,0)) . (Bottom P) & 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,0)) . (Bottom P) ) } holds z <= sup M let M be non empty Chain of P; ::_thesis: ( z = (iter (g0,0)) . (Bottom P) & 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,0)) . (Bottom P) ) } implies z <= sup M ) assume z = (iter (g0,0)) . (Bottom P) ; ::_thesis: ( not 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,0)) . (Bottom P) ) } or z <= sup M ) then z = Bottom P by Lm5; hence ( not 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,0)) . (Bottom P) ) } or z <= sup M ) by YELLOW_0:44; ::_thesis: verum end; A11: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A12: S1[k] ; ::_thesis: S1[k + 1] for z1 being Element of P for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { 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,(k + 1))) . (Bottom P) ) } holds z1 <= sup M1 proof let z1 be Element of P; ::_thesis: for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { 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,(k + 1))) . (Bottom P) ) } holds z1 <= sup M1 let M1 be non empty Chain of P; ::_thesis: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { 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,(k + 1))) . (Bottom P) ) } implies z1 <= sup M1 ) assume A13: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 = { 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,(k + 1))) . (Bottom P) ) } ) ; ::_thesis: z1 <= sup M1 reconsider z = (iter (g0,k)) . (Bottom P) as Element of P by Lm6; A14: z1 = (g0 * (iter (g0,k))) . (Bottom P) by A13, FUNCT_7:71 .= g0 . z by Lm7 ; reconsider 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,k)) . (Bottom P) ) } as non empty Chain of P by Lm37; reconsider M0 = g0 .: M as non empty Chain of P by Th1; A15: g0 . (sup M) = sup M0 by Th6; A16: ex_sup_of M0,P by Def1; for q being Element of P st q in M0 holds q <= sup M1 proof let q be Element of P; ::_thesis: ( q in M0 implies q <= sup M1 ) assume q in M0 ; ::_thesis: q <= sup M1 then consider g being continuous Function of P,P such that A17: ( g in G & q = g0 . ((iter (g,k)) . (Bottom P)) ) by Lm40; reconsider a1 = (iter (g,k)) . (Bottom P) as Element of P by Lm6; reconsider W = G -image a1 as non empty Chain of P ; A18: q = sup W by A17, Def10, A2; A19: ex_sup_of W,P by Def1; for q1 being Element of P st q1 in W holds q1 <= sup M1 proof let q1 be Element of P; ::_thesis: ( q1 in W implies q1 <= sup M1 ) assume q1 in W ; ::_thesis: q1 <= sup M1 then consider q2 being Element of P such that A20: ( q1 = q2 & ex g1 being continuous Function of P,P st ( g1 in G & q2 = g1 . a1 ) ) ; consider g1 being continuous Function of P,P such that A21: ( g1 in G & q1 = g1 . a1 ) by A20; percases ( g1 <= g or g <= g1 ) by A17, A21, Lm36; suppose g1 <= g ; ::_thesis: q1 <= sup M1 then A22: q1 <= g . a1 by A21, YELLOW_2:9; set a2 = g . a1; reconsider g2 = g as Element of (ConPoset (P,P)) by Lm30; reconsider gg = g2 as continuous Function of P,P ; g . a1 = (g * (iter (g,k))) . (Bottom P) by Lm7 .= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ; then g . a1 in M1 by A13, A17; then g . a1 <= sup M1 by Lm23; hence q1 <= sup M1 by A22, ORDERS_2:3; ::_thesis: verum end; supposeA23: g <= g1 ; ::_thesis: q1 <= sup M1 reconsider a2 = (iter (g1,k)) . (Bottom P) as Element of P by Lm6; a1 <= a2 by A23, Lm12; then A24: q1 <= g1 . a2 by A21, ORDERS_3:def_5; set a3 = g1 . a2; reconsider g2 = g1 as Element of (ConPoset (P,P)) by Lm30; reconsider gg = g2 as continuous Function of P,P ; g1 . a2 = (g1 * (iter (g1,k))) . (Bottom P) by Lm7 .= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ; then g1 . a2 in M1 by A13, A21; then g1 . a2 <= sup M1 by Lm23; hence q1 <= sup M1 by A24, ORDERS_2:3; ::_thesis: verum end; end; end; then W is_<=_than sup M1 by LATTICE3:def_9; hence q <= sup M1 by A18, A19, YELLOW_0:def_9; ::_thesis: verum end; then M0 is_<=_than sup M1 by LATTICE3:def_9; then A25: sup M0 <= sup M1 by A16, YELLOW_0:def_9; z <= sup M by A12; then z1 <= sup M0 by A14, A15, ORDERS_3:def_5; hence z1 <= sup M1 by A25, ORDERS_2:3; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A10, A11); then x <= sup M0 by A6; hence x <= sup L by A9, ORDERS_2:3; ::_thesis: verum end; then I0 is_<=_than sup L by LATTICE3:def_9; hence h . (sup G) <= sup (h .: G) by A3, A4, YELLOW_0:def_9; ::_thesis: verum end; hence (fix_func P) . (sup G) <= sup ((fix_func P) .: G) ; ::_thesis: verum end; registration let P be non empty strict chain-complete Poset; cluster fix_func P -> continuous ; coherence fix_func P is continuous proof reconsider f = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm32; for L being non empty Chain of (ConPoset (P,P)) holds f . (sup L) <= sup (f .: L) by Lm41; hence fix_func P is continuous by Th8; ::_thesis: verum end; end;