KNASTER: Fix-points in complete lattices

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

theorem :: KNASTER:1

canceled;

theorem :: KNASTER:2

canceled;

theorem :: KNASTER:3

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

proof end;

theorem Th4: :: KNASTER:4

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

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;
canceled;
canceled;
:: original: c=-monotone
redefine attr f is c=-monotone means :Def3: :: KNASTER:def 3
for x, y being Element of A st x c= y holds
f . x c= f . y;
compatibility

proof end;

end;

:: deftheorem KNASTER:def 1 :

:: deftheorem KNASTER:def 2 :

:: deftheorem Def3 defines c=-monotone KNASTER:def 3 :

registration

let A be set ;
let B be non empty set ;
cluster c=-monotone Relation of A,B;
existence

proof end;

end;

definition

let X be set ;
let f be V197 Function of bool X, bool X;
func lfp X,f -> Subset of X equals :: KNASTER:def 4
meet { h where h is Subset of X : f . h c= h } ;
coherence

proof end;

func gfp X,f -> Subset of X equals :: KNASTER:def 5
union { h where h is Subset of X : h c= f . h } ;
coherence

proof end;

end;

:: deftheorem defines lfp KNASTER:def 4 :

:: deftheorem defines gfp KNASTER:def 5 :

theorem Th6: :: KNASTER:6

for X being set
for f being V197 Function of bool X, bool X holds lfp X,f is_a_fixpoint_of f

proof end;

theorem Th7: :: KNASTER:7

for X being set
for f being V197 Function of bool X, bool X holds gfp X,f is_a_fixpoint_of f

proof end;

theorem Th8: :: KNASTER:8

for X being set
for f being V197 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 Th9: :: KNASTER:9

for X being set
for f being V197 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 Th10: :: KNASTER:10

for X being set
for f being V197 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 )

proof end;

scheme :: KNASTER:sch 1
Knaster{ F₁() -> set , F₂( set ) -> set } :

ex D being set st
( F₂(D) = D & D c= F₁() )

provided

A1: for X, Y being set st X c= Y holds
F₂(X) c= F₂(Y) and
A2: F₂(F₁()) c= F₁()

proof end;

theorem Th11: :: KNASTER:11

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;

theorem Th12: :: 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
ex h being Function of X,Y st h is bijective

proof end;

theorem Th13: :: KNASTER:13

for Y, X being non empty set st ex f being Function of X,Y st f is bijective holds
X,Y are_equipotent

proof end;

theorem :: KNASTER:14

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 :Def6: :: KNASTER:def 6
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

proof end;

func f,O -. x -> set means :Def7: :: KNASTER:def 7
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

proof end;

end;

:: deftheorem Def6 defines +. KNASTER:def 6 :

:: deftheorem Def7 defines -. KNASTER:def 7 :

theorem :: KNASTER:15

canceled;

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 holds f,{} +. x = 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 holds f,{} -. x = x

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 holds f,(succ O) +. x = f . (f,O +. x)

proof end;

theorem Th19: :: KNASTER:19

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 Th20: :: KNASTER:20

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

proof end;

theorem Th21: :: KNASTER:21

proof end;

theorem :: KNASTER:22

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

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

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

proof end;

end;

definition

let L be non empty LattStr ;
let P be Subset of L;
attr P is with_suprema means :Def8: :: KNASTER:def 8
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 z' being Element of L st z' in P & x [= z' & y [= z' holds
z [= z' ) );
attr P is with_infima means :Def9: :: KNASTER:def 9
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 z' being Element of L st z' in P & z' [= x & z' [= y holds
z' [= z ) );

end;

:: deftheorem Def8 defines with_suprema KNASTER:def 8 :

:: deftheorem Def9 defines with_infima KNASTER:def 9 :

registration

let L be Lattice;
cluster non empty with_suprema with_infima Element of bool the carrier of L;
existence

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 :Def10: :: KNASTER:def 10
( the carrier of it = P & ( for x, y being Element of it ex x', y' being Element of L st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines latt KNASTER:def 10 :

registration

cluster complete -> bounded LattStr ;
coherence

proof end;

end;

theorem Th24: :: KNASTER:24

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 Th25: :: KNASTER:25

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 Th26: :: KNASTER:26

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 Th27: :: KNASTER:27

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 Th28: :: KNASTER:28

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 Th29: :: KNASTER:29

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 Th30: :: KNASTER:30

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 Th31: :: KNASTER:31

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 Th32: :: KNASTER:32

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 Th33: :: KNASTER:33

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 Th34: :: KNASTER:34

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 Th35: :: KNASTER:35

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 Th36: :: KNASTER:36

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 Th37: :: KNASTER:37

for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st a [= f . a & a [= b & b is_a_fixpoint_of f holds
for O2 being Ordinal holds f,O2 +. a [= b

proof end;

theorem Th38: :: KNASTER:38

for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st f . a [= a & 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 :Def11: :: KNASTER:def 11
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

proof end;

uniqueness ;

end;

:: deftheorem Def11 defines FixPoints KNASTER:def 11 :

theorem Th39: :: KNASTER:39

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 }

proof end;

theorem Th40: :: KNASTER:40

for L being complete Lattice
for f being monotone UnOp of L holds the carrier of (FixPoints f) c= the carrier of L

proof end;

theorem Th41: :: KNASTER:41

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 )

proof end;

theorem Th42: :: KNASTER:42

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 )

proof end;

theorem :: KNASTER:43

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 12
f,(nextcard the carrier of L) +. (Bottom L);
coherence ;
func gfp f -> Element of L equals :: KNASTER:def 13
f,(nextcard the carrier of L) -. (Top L);
coherence ;

end;

:: deftheorem defines lfp KNASTER:def 12 :

:: deftheorem defines gfp KNASTER:def 13 :

theorem Th44: :: KNASTER:44

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

proof end;

theorem Th45: :: KNASTER:45

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 Th46: :: KNASTER:46

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

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

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 Th49: :: KNASTER:49

for A being non empty set
for f being UnOp of (BooleLatt A) holds
( f is monotone iff f is c=-monotone )

proof end;

theorem :: KNASTER:50

for A being non empty set
for f being monotone UnOp of (BooleLatt A) ex g being V197 Function of bool A, bool A st lfp A,g = lfp f

proof end;

theorem :: KNASTER:51

for A being non empty set
for f being monotone UnOp of (BooleLatt A) ex g being V197 Function of bool A, bool A st gfp A,g = gfp f

proof end;