:: Fix-points in complete lattices
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Copyright (c) 1996-2021 Association of Mizar Users

theorem :: KNASTER:1
for f, g, h 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 ) )
proof end;

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)
proof end;

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
proof end;

definition
let A, B be non empty set ;
let f be Function of A,B;
:: original: c=-monotone
redefine attr f 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 )
proof end;
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 ;
existence
ex b1 being Function of A,B st b1 is c=-monotone
proof end;
end;

definition
let X be set ;
let f be V224() 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
proof end;
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
proof end;
end;

:: deftheorem defines lfp KNASTER:def 2 :
for X being set
for f being V224() 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 V224() 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 V224() Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f
proof end;

theorem Th5: :: KNASTER:5
for X being set
for f being V224() Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f
proof end;

theorem Th6: :: KNASTER:6
for X being set
for f being V224() Function of (bool X),(bool X)
for S being Subset of X st f . S c= S holds
lfp (X,f) c= S
proof end;

theorem Th7: :: KNASTER:7
for X being set
for f being V224() Function of (bool X),(bool X)
for S being Subset of X st S c= f . S holds
S c= gfp (X,f)
proof end;

theorem Th8: :: KNASTER:8
for X being set
for f being V224() 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) ) by ;

:: Knaster Theorem
scheme :: KNASTER:sch 1
Knaster{ F1() -> set , F2( object ) -> 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()
proof end;

:: 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 )
proof end;

:: 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
proof end;

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
proof end;

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
proof end;

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 Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) )
;
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) holds
b1 = b2
;
proof end;
func (f,O) -. x -> set means :Def5: :: KNASTER:def 5
ex L0 being Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) )
;
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) holds
b1 = b2
;
proof end;
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 Sequence st
( b5 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & 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 Sequence st
( b5 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & 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,0) +. x = x
proof end;

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,0) -. x = x
proof end;

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)
proof end;

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)
proof end;

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 Sequence st O <> 0 & 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)
proof end;

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 Sequence st O <> 0 & 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)
proof end;

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
proof end;

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
proof 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
proof end;
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
proof end;
end;

definition
let L be non empty LattStr ;
let P be Subset of L;
attr P 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 ) );
attr P 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 )
proof end;
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 ) ) ) )
proof end;
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
proof end;
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 ) ) ) ) );

registration
coherence
for b1 being Lattice st b1 is complete holds
b1 is bounded
proof end;
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

Lm1: for O1, O2 being Ordinal holds
( O1 c< O2 or O1 = O2 or O2 c< O1 )

proof end;

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 )
proof end;

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 )
proof end;

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) )
proof end;

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 )
proof end;

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
proof end;

theorem Th35: :: KNASTER:35
for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a
proof end;

definition
let L be complete Lattice;
let f be UnOp of L;
assume A1: 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 )
proof end;
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 () = { x where x is Element of L : x is_a_fixpoint_of f }
proof end;

theorem Th37: :: KNASTER:37
for L being complete Lattice
for f being monotone UnOp of L holds the carrier of () c= the carrier of L
proof end;

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 () iff a is_a_fixpoint_of f )
proof end;

theorem Th39: :: KNASTER:39
for L being complete Lattice
for f being monotone UnOp of L
for x, y being Element of ()
for a, b being Element of L st x = a & y = b holds
( x [= y iff a [= b )
proof end;

theorem :: KNASTER:40
for L being complete Lattice
for f being monotone UnOp of L holds FixPoints f is complete
proof end;

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)) +. ();
coherence
(f,(nextcard the carrier of 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)) +. ();

:: 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) +. () = lfp f ) )
proof end;

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 ) )
proof end;

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 )
proof end;

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
proof end;

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
proof end;

theorem Th46: :: KNASTER:46
for A being non empty set
for f being UnOp of () holds
( f is monotone iff f is V224() )
proof end;

theorem :: KNASTER:47
for A being non empty set
for f being monotone UnOp of () ex g being V224() Function of (bool A),(bool A) st lfp (A,g) = lfp f
proof end;

theorem :: KNASTER:48
for A being non empty set
for f being monotone UnOp of () ex g being V224() Function of (bool A),(bool A) st gfp (A,g) = gfp f
proof end;