:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received September 16, 1996

:: 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 ) )

( 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)

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

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;

( f is c=-monotone iff for x, y being Element of A st x c= y holds

f . x c= f . y )

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

( f is c=-monotone iff for x, y being Element of A st x c= y holds

f . x c= f . y )

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

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 ;

ex b_{1} being Function of A,B st b_{1} is c=-monotone

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

proof end;

definition

let X be set ;

let f be V224() Function of (bool X),(bool X);

meet { h where h is Subset of X : f . h c= h } is Subset of X

union { h where h is Subset of X : h c= f . h } is Subset of X

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

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 } ;

union { h where h is Subset of X : h c= f . h } is Subset of X

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

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 } ;

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 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

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)

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;

:: Knaster Theorem

:: 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 )

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;

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

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 :: 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

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;

existence

ex b_{1} being set ex L0 being Sequence st

( b_{1} = 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 b_{1}, b_{2} being set st ex L0 being Sequence st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2};

existence

ex b_{1} being set ex L0 being Sequence st

( b_{1} = 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 b_{1}, b_{2} being set st ex L0 being Sequence st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2};

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

existence

ex b

( b

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 b

( b

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

( b

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

b

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

existence

ex b

( b

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 b

( b

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

( b

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

b

proof 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 b_{5} being set holds

( b_{5} = (f,O) +. x iff ex L0 being Sequence st

( b_{5} = 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) ) ) );

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 b

( b

( b

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 b_{5} being set holds

( b_{5} = (f,O) -. x iff ex L0 being Sequence st

( b_{5} = 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) ) ) );

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 b

( b

( b

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

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

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)

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)

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)

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)

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

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

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

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

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

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

definition

let L be non empty LattStr ;

let P be Subset of L;

end;
let P be Subset of L;

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

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

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;

existence

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is with_suprema & b_{1} is with_infima )

end;
existence

ex b

( not b

proof end;

definition

let L be Lattice;

let P be non empty with_suprema with_infima Subset of L;

ex b_{1} being strict Lattice st

( the carrier of b_{1} = P & ( for x, y being Element of b_{1} ex x9, y9 being Element of L st

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) )

for b_{1}, b_{2} being strict Lattice st the carrier of b_{1} = P & ( for x, y being Element of b_{1} 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 b_{2} = P & ( for x, y being Element of b_{2} ex x9, y9 being Element of L st

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) )

proof end;

uniqueness for b

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) & the carrier of b

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) holds

b

proof 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 b_{3} being strict Lattice holds

( b_{3} = latt P iff ( the carrier of b_{3} = P & ( for x, y being Element of b_{3} ex x9, y9 being Element of L st

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) );

for L being Lattice

for P being non empty with_suprema with_infima Subset of L

for b

( b

( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) );

registration
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

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

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

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

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

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

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

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

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

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 )

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 )

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) )

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 )

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

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

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 ;

ex b_{1} 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 } & b_{1} = latt P )

for b_{1}, b_{2} 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 } & b_{1} = 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 } & b_{2} = latt P ) holds

b_{1} = b_{2}
;

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

ex b

( P = { x where x is Element of L : x is_a_fixpoint_of f } & b

proof end;

uniqueness for b

( P = { x where x is Element of L : x is_a_fixpoint_of f } & b

( P = { x where x is Element of L : x is_a_fixpoint_of f } & b

b

:: deftheorem Def9 defines FixPoints KNASTER:def 9 :

for L being complete Lattice

for f being UnOp of L st f is monotone holds

for b_{3} being strict Lattice holds

( b_{3} = 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 } & b_{3} = latt P ) );

for L being complete Lattice

for f being UnOp of L st f is monotone holds

for b

( b

( P = { x where x is Element of L : x is_a_fixpoint_of f } & b

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 }

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 }

proof end;

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

for f being monotone UnOp of L holds the carrier of (FixPoints f) 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 (FixPoints f) iff a is_a_fixpoint_of f )

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 )

proof end;

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 )

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 )

proof end;

definition

let L be complete Lattice;

let f be monotone UnOp of L;

coherence

(f,(nextcard the carrier of L)) +. (Bottom L) is Element of L ;

coherence

(f,(nextcard the carrier of L)) -. (Top L) is Element of L ;

end;
let f be monotone UnOp of L;

coherence

(f,(nextcard the carrier of L)) +. (Bottom L) is Element of L ;

coherence

(f,(nextcard the carrier of L)) -. (Top L) is Element of L ;

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

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

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 ) )

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 ) )

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 ) )

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 )

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

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

for f being monotone UnOp of L

for a being Element of L st a [= f . a holds

a [= gfp f

proof end;

theorem :: KNASTER:47

for A being non empty set

for f being monotone UnOp of (BooleLatt A) ex g being V224() Function of (bool A),(bool A) st lfp (A,g) = lfp f

for f being monotone UnOp of (BooleLatt A) 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 (BooleLatt A) ex g being V224() Function of (bool A),(bool A) st gfp (A,g) = gfp f

for f being monotone UnOp of (BooleLatt A) ex g being V224() Function of (bool A),(bool A) st gfp (A,g) = gfp f

proof end;