:: Fix-points in complete lattices :: by Piotr Rudnicki and Andrzej Trybulec :: :: Received September 16, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin theorem :: KNASTER:1 for h, f, g being Function st h = f \/ g & dom f misses dom g holds ( h is one-to-one iff ( f is one-to-one & g is one-to-one & rng f misses rng g ) ) proofend; begin theorem Th2: :: KNASTER:2 for X, x being set for n being Element of NAT for f being Function of X,X st x is_a_fixpoint_of iter (f,n) holds f . x is_a_fixpoint_of iter (f,n) proofend; theorem :: KNASTER:3 for X, x being set for f being Function of X,X st ex n being Element of NAT st ( x is_a_fixpoint_of iter (f,n) & ( for y being set st y is_a_fixpoint_of iter (f,n) holds x = y ) ) holds x is_a_fixpoint_of f proofend; definition let A, B be non empty set ; let f be Function of A,B; :: original:c=-monotone redefine attrf is c=-monotone means :Def1: :: KNASTER:def 1 for x, y being Element of A st x c= y holds f . x c= f . y; compatibility ( f is c=-monotone iff for x, y being Element of A st x c= y holds f . x c= f . y ) proofend; end; :: deftheorem Def1 defines c=-monotone KNASTER:def_1_:_ for A, B being non empty set for f being Function of A,B holds ( f is c=-monotone iff for x, y being Element of A st x c= y holds f . x c= f . y ); registration let A be set ; let B be non empty set ; cluster Relation-like A -defined B -valued Function-like quasi_total c=-monotone for Element of bool [:A,B:]; existence ex b1 being Function of A,B st b1 is c=-monotone proofend; end; definition let X be set ; let f be V220() Function of (bool X),(bool X); func lfp (X,f) -> Subset of X equals :: KNASTER:def 2 meet { h where h is Subset of X : f . h c= h } ; coherence meet { h where h is Subset of X : f . h c= h } is Subset of X proofend; func gfp (X,f) -> Subset of X equals :: KNASTER:def 3 union { h where h is Subset of X : h c= f . h } ; coherence union { h where h is Subset of X : h c= f . h } is Subset of X proofend; end; :: deftheorem defines lfp KNASTER:def_2_:_ for X being set for f being V220() Function of (bool X),(bool X) holds lfp (X,f) = meet { h where h is Subset of X : f . h c= h } ; :: deftheorem defines gfp KNASTER:def_3_:_ for X being set for f being V220() Function of (bool X),(bool X) holds gfp (X,f) = union { h where h is Subset of X : h c= f . h } ; theorem Th4: :: KNASTER:4 for X being set for f being V220() Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f proofend; theorem Th5: :: KNASTER:5 for X being set for f being V220() Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f proofend; theorem Th6: :: KNASTER:6 for X being set for f being V220() Function of (bool X),(bool X) for S being Subset of X st f . S c= S holds lfp (X,f) c= S proofend; theorem Th7: :: KNASTER:7 for X being set for f being V220() Function of (bool X),(bool X) for S being Subset of X st S c= f . S holds S c= gfp (X,f) proofend; theorem Th8: :: KNASTER:8 for X being set for f being V220() Function of (bool X),(bool X) for S being Subset of X st S is_a_fixpoint_of f holds ( lfp (X,f) c= S & S c= gfp (X,f) ) proofend; scheme :: KNASTER:sch 1 Knaster{ F1() -> set , F2( set ) -> set } : ex D being set st ( F2(D) = D & D c= F1() ) provided A1: for X, Y being set st X c= Y holds F2(X) c= F2(Y) and A2: F2(F1()) c= F1() proofend; :: Banach decomposition theorem Th9: :: KNASTER:9 for X, Y being non empty set for f being Function of X,Y for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb ) proofend; :: [WP: ] Schroeder_Bernstein_theorem theorem Th10: :: KNASTER:10 for X, Y being non empty set for f being Function of X,Y for g being Function of Y,X st f is one-to-one & g is one-to-one holds ex h being Function of X,Y st h is bijective proofend; theorem Th11: :: KNASTER:11 for X, Y being non empty set for f being Function of X,Y st f is bijective holds X,Y are_equipotent proofend; theorem :: KNASTER:12 for X, Y being non empty set for f being Function of X,Y for g being Function of Y,X st f is one-to-one & g is one-to-one holds X,Y are_equipotent proofend; begin definition let L be Lattice; let f be Function of the carrier of L, the carrier of L; let x be Element of L; let O be Ordinal; func(f,O) +. x -> set means :Def4: :: KNASTER:def 4 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "\/" ((rng (L0 | C)),L) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "\/" ((rng (L0 | C)),L) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "\/" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "\/" ((rng (L0 | C)),L) ) ) holds b1 = b2; proofend; func(f,O) -. x -> set means :Def5: :: KNASTER:def 5 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "/\" ((rng (L0 | C)),L) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "/\" ((rng (L0 | C)),L) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "/\" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "/\" ((rng (L0 | C)),L) ) ) holds b1 = b2; proofend; end; :: deftheorem Def4 defines +. KNASTER:def_4_:_ for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal for b5 being set holds ( b5 = (f,O) +. x iff ex L0 being T-Sequence st ( b5 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "\/" ((rng (L0 | C)),L) ) ) ); :: deftheorem Def5 defines -. KNASTER:def_5_:_ for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal for b5 being set holds ( b5 = (f,O) -. x iff ex L0 being T-Sequence st ( b5 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = "/\" ((rng (L0 | C)),L) ) ) ); theorem Th13: :: KNASTER:13 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L holds (f,{}) +. x = x proofend; theorem Th14: :: KNASTER:14 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L holds (f,{}) -. x = x proofend; theorem Th15: :: KNASTER:15 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x) proofend; theorem Th16: :: KNASTER:16 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal holds (f,(succ O)) -. x = f . ((f,O) -. x) proofend; theorem Th17: :: KNASTER:17 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds T . A = (f,A) +. x ) holds (f,O) +. x = "\/" ((rng T),L) proofend; theorem Th18: :: KNASTER:18 for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L for O being Ordinal for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds T . A = (f,A) -. x ) holds (f,O) -. x = "/\" ((rng T),L) proofend; theorem :: KNASTER:19 for n being Element of NAT for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L holds (iter (f,n)) . x = (f,n) +. x proofend; theorem :: KNASTER:20 for n being Element of NAT for L being Lattice for f being Function of the carrier of L, the carrier of L for x being Element of L holds (iter (f,n)) . x = (f,n) -. x proofend; definition let L be Lattice; let f be UnOp of the carrier of L; let a be Element of L; let O be Ordinal; :: original:+. redefine func(f,O) +. a -> Element of L; coherence (f,O) +. a is Element of L proofend; end; definition let L be Lattice; let f be UnOp of the carrier of L; let a be Element of L; let O be Ordinal; :: original:-. redefine func(f,O) -. a -> Element of L; coherence (f,O) -. a is Element of L proofend; end; definition let L be non empty LattStr ; let P be Subset of L; attrP is with_suprema means :Def6: :: KNASTER:def 6 for x, y being Element of L st x in P & y in P holds ex z being Element of L st ( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds z [= z9 ) ); attrP is with_infima means :Def7: :: KNASTER:def 7 for x, y being Element of L st x in P & y in P holds ex z being Element of L st ( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z ) ); end; :: deftheorem Def6 defines with_suprema KNASTER:def_6_:_ for L being non empty LattStr for P being Subset of L holds ( P is with_suprema iff for x, y being Element of L st x in P & y in P holds ex z being Element of L st ( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds z [= z9 ) ) ); :: deftheorem Def7 defines with_infima KNASTER:def_7_:_ for L being non empty LattStr for P being Subset of L holds ( P is with_infima iff for x, y being Element of L st x in P & y in P holds ex z being Element of L st ( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z ) ) ); registration let L be Lattice; cluster non empty with_suprema with_infima for Element of bool the carrier of L; existence ex b1 being Subset of L st ( not b1 is empty & b1 is with_suprema & b1 is with_infima ) proofend; end; definition let L be Lattice; let P be non empty with_suprema with_infima Subset of L; func latt P -> strict Lattice means :Def8: :: KNASTER:def 8 ( the carrier of it = P & ( for x, y being Element of it ex x9, y9 being Element of L st ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ); existence ex b1 being strict Lattice st ( the carrier of b1 = P & ( for x, y being Element of b1 ex x9, y9 being Element of L st ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) proofend; uniqueness for b1, b2 being strict Lattice st the carrier of b1 = P & ( for x, y being Element of b1 ex x9, y9 being Element of L st ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) & the carrier of b2 = P & ( for x, y being Element of b2 ex x9, y9 being Element of L st ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines latt KNASTER:def_8_:_ for L being Lattice for P being non empty with_suprema with_infima Subset of L for b3 being strict Lattice holds ( b3 = latt P iff ( the carrier of b3 = P & ( for x, y being Element of b3 ex x9, y9 being Element of L st ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) ); begin registration cluster non empty Lattice-like complete -> bounded for LattStr ; coherence for b1 being Lattice st b1 is complete holds b1 is bounded proofend; end; theorem Th21: :: KNASTER:21 for L being complete Lattice for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f proofend; theorem Th22: :: KNASTER:22 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a holds for O being Ordinal holds a [= (f,O) +. a proofend; theorem Th23: :: KNASTER:23 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a holds for O being Ordinal holds (f,O) -. a [= a proofend; theorem Th24: :: KNASTER:24 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a holds for O1, O2 being Ordinal st O1 c= O2 holds (f,O1) +. a [= (f,O2) +. a proofend; theorem Th25: :: KNASTER:25 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a holds for O1, O2 being Ordinal st O1 c= O2 holds (f,O2) -. a [= (f,O1) -. a proofend; theorem Th26: :: KNASTER:26 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a holds for O1, O2 being Ordinal st O1 c< O2 & not (f,O2) +. a is_a_fixpoint_of f holds (f,O1) +. a <> (f,O2) +. a proofend; theorem Th27: :: KNASTER:27 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a holds for O1, O2 being Ordinal st O1 c< O2 & not (f,O2) -. a is_a_fixpoint_of f holds (f,O1) -. a <> (f,O2) -. a proofend; theorem Th28: :: KNASTER:28 for O1 being Ordinal for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds for O2 being Ordinal st O1 c= O2 holds (f,O1) +. a = (f,O2) +. a proofend; theorem Th29: :: KNASTER:29 for O1 being Ordinal for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds for O2 being Ordinal st O1 c= O2 holds (f,O1) -. a = (f,O2) -. a proofend; Lm1: for O1, O2 being Ordinal holds ( O1 c< O2 or O1 = O2 or O2 c< O1 ) proofend; theorem Th30: :: KNASTER:30 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a holds ex O being Ordinal st ( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f ) proofend; theorem Th31: :: KNASTER:31 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a holds ex O being Ordinal st ( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f ) proofend; theorem Th32: :: KNASTER:32 for L being complete Lattice for f being monotone UnOp of L for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds ex O being Ordinal st ( card O c= card the carrier of L & (f,O) +. (a "\/" b) is_a_fixpoint_of f & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" b) ) proofend; theorem Th33: :: KNASTER:33 for L being complete Lattice for f being monotone UnOp of L for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds ex O being Ordinal st ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b ) proofend; theorem Th34: :: KNASTER:34 for L being complete Lattice for f being monotone UnOp of L for a, b being Element of L st a [= b & b is_a_fixpoint_of f holds for O2 being Ordinal holds (f,O2) +. a [= b proofend; theorem Th35: :: KNASTER:35 for L being complete Lattice for f being monotone UnOp of L for b, a being Element of L st b [= a & b is_a_fixpoint_of f holds for O2 being Ordinal holds b [= (f,O2) -. a proofend; definition let L be complete Lattice; let f be UnOp of L; assume B1: f is monotone ; func FixPoints f -> strict Lattice means :Def9: :: KNASTER:def 9 ex P being non empty with_suprema with_infima Subset of L st ( P = { x where x is Element of L : x is_a_fixpoint_of f } & it = latt P ); existence ex b1 being strict Lattice ex P being non empty with_suprema with_infima Subset of L st ( P = { x where x is Element of L : x is_a_fixpoint_of f } & b1 = latt P ) proofend; uniqueness for b1, b2 being strict Lattice st ex P being non empty with_suprema with_infima Subset of L st ( P = { x where x is Element of L : x is_a_fixpoint_of f } & b1 = latt P ) & ex P being non empty with_suprema with_infima Subset of L st ( P = { x where x is Element of L : x is_a_fixpoint_of f } & b2 = latt P ) holds b1 = b2 ; end; :: deftheorem Def9 defines FixPoints KNASTER:def_9_:_ for L being complete Lattice for f being UnOp of L st f is monotone holds for b3 being strict Lattice holds ( b3 = FixPoints f iff ex P being non empty with_suprema with_infima Subset of L st ( P = { x where x is Element of L : x is_a_fixpoint_of f } & b3 = latt P ) ); theorem Th36: :: KNASTER:36 for L being complete Lattice for f being monotone UnOp of L holds the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } proofend; theorem Th37: :: KNASTER:37 for L being complete Lattice for f being monotone UnOp of L holds the carrier of (FixPoints f) c= the carrier of L proofend; theorem Th38: :: KNASTER:38 for L being complete Lattice for f being monotone UnOp of L for a being Element of L holds ( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f ) proofend; theorem Th39: :: KNASTER:39 for L being complete Lattice for f being monotone UnOp of L for x, y being Element of (FixPoints f) for a, b being Element of L st x = a & y = b holds ( x [= y iff a [= b ) proofend; theorem :: KNASTER:40 for L being complete Lattice for f being monotone UnOp of L holds FixPoints f is complete proofend; definition let L be complete Lattice; let f be monotone UnOp of L; func lfp f -> Element of L equals :: KNASTER:def 10 (f,(nextcard the carrier of L)) +. (Bottom L); coherence (f,(nextcard the carrier of L)) +. (Bottom L) is Element of L ; func gfp f -> Element of L equals :: KNASTER:def 11 (f,(nextcard the carrier of L)) -. (Top L); coherence (f,(nextcard the carrier of L)) -. (Top L) is Element of L ; end; :: deftheorem defines lfp KNASTER:def_10_:_ for L being complete Lattice for f being monotone UnOp of L holds lfp f = (f,(nextcard the carrier of L)) +. (Bottom L); :: deftheorem defines gfp KNASTER:def_11_:_ for L being complete Lattice for f being monotone UnOp of L holds gfp f = (f,(nextcard the carrier of L)) -. (Top L); theorem Th41: :: KNASTER:41 for L being complete Lattice for f being monotone UnOp of L holds ( lfp f is_a_fixpoint_of f & ex O being Ordinal st ( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) ) proofend; theorem Th42: :: KNASTER:42 for L being complete Lattice for f being monotone UnOp of L holds ( gfp f is_a_fixpoint_of f & ex O being Ordinal st ( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) ) proofend; theorem Th43: :: KNASTER:43 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a is_a_fixpoint_of f holds ( lfp f [= a & a [= gfp f ) proofend; theorem :: KNASTER:44 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st f . a [= a holds lfp f [= a proofend; theorem :: KNASTER:45 for L being complete Lattice for f being monotone UnOp of L for a being Element of L st a [= f . a holds a [= gfp f proofend; begin theorem Th46: :: KNASTER:46 for A being non empty set for f being UnOp of (BooleLatt A) holds ( f is monotone iff f is V220() ) proofend; theorem :: KNASTER:47 for A being non empty set for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st lfp (A,g) = lfp f proofend; theorem :: KNASTER:48 for A being non empty set for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f proofend;