Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Fixpoints in Complete Lattices

by
Piotr Rudnicki, and
Andrzej Trybulec

Received September 16, 1996

MML identifier: KNASTER
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, COHSP_1, FUNCOP_1, SETFAM_1,
TARSKI, SGRAPH1, CARD_1, LATTICES, BINOP_1, ORDINAL1, ORDINAL2, LATTICE3,
FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1, BHSP_3, SEQM_3, KNASTER,
PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, RELAT_2,
RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1,
SETFAM_1, FUNCT_4, WELLORD1, ORDINAL1, ORDINAL2, CARD_1, COHSP_1,
LATTICES, LATTICE3, QUANTAL1, ORDERS_1, FUNCT_7;
constructors NAT_1, BINOP_1, DOMAIN_1, WELLORD2, COHSP_1, BOOLEALG, QUANTAL1,
PROB_1, FUNCT_7, WELLORD1;
clusters SUBSET_1, STRUCT_0, FUNCT_1, LATTICES, CARD_1, LATTICE3, RELSET_1,
ORDINAL1, QUANTAL1;
requirements NUMERALS, BOOLE, SUBSET;

begin :: Preliminaries

reserve f, g, h for Function;

theorem :: KNASTER:1
f is one-to-one & g is one-to-one & rng f misses rng g
implies f+*g is one-to-one;

canceled;

theorem :: KNASTER:3
h = f \/ g & dom f misses dom g implies
(h is one-to-one iff f is one-to-one & g is one-to-one & rng f misses rng g);

begin :: Fix points in general

definition
let x be set, f be Function;
pred x is_a_fixpoint_of f means
:: KNASTER:def 1
x in dom f & x = f.x;
end;

definition
let A be non empty set, a be Element of A, f be Function of A, A;
redefine pred a is_a_fixpoint_of f means
:: KNASTER:def 2
a = f.a;
end;

reserve x, y, z, u, X for set,
A for non empty set,
n for Nat,
f for Function of X, X;

theorem :: KNASTER:4
x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f,n);

theorem :: KNASTER:5
(ex n st x is_a_fixpoint_of iter(f,n) &
for y st y is_a_fixpoint_of iter(f,n) holds x = y)
implies x is_a_fixpoint_of f;

definition let A, B be non empty set, f be Function of A, B;
redefine attr f is c=-monotone means
:: KNASTER:def 3
for x, y being Element of A st x c= y holds f.x c= f.y;
end;

definition let A be set, B be non empty set;
cluster c=-monotone Function of A, B;
end;

definition let X be set;
let f be c=-monotone 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};
func gfp (X, f) -> Subset of X equals
:: KNASTER:def 5
union {h where h is Subset of X : h c= f.h };
end;

reserve f for c=-monotone Function of bool X, bool X,
S for Subset of X;

theorem :: KNASTER:6
lfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:7
gfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:8
f.S c= S implies lfp(X,f) c= S;

theorem :: KNASTER:9
S c= f.S implies S c= gfp(X,f);

theorem :: KNASTER:10
S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f);

scheme Knaster{A() -> set, F(set) -> set}:
ex D being set st F(D) = D & D c= A()
provided
for X, Y being set st X c= Y holds F(X) c= F(Y) and
F(A()) c= A();

reserve X, Y for non empty set,
f for Function of X, Y,
g for Function of Y, X;

theorem :: KNASTER:11  :: Banach decomposition
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;

theorem :: KNASTER:12  :: Schroeder-Bernstein
f is one-to-one & g is one-to-one implies
ex h being Function of X,Y st h is bijective;

theorem :: KNASTER:13
(ex f st f is bijective) implies X,Y are_equipotent;

theorem :: KNASTER:14
f is one-to-one & g is one-to-one implies X,Y are_equipotent;

begin :: The lattice of a lattice subset

definition
let L be non empty LattStr, f be UnOp of L, x be Element of L;
redefine func f.x -> Element of L;
end;

definition
let L be Lattice, f be Function of the carrier of L, the carrier of L,
x be Element of L, O be Ordinal;
func (f, O)+.x means
:: 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);
func (f, O)-.x means
:: 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);
end;

reserve L for Lattice,
f for Function of the carrier of L, the carrier of L,
x for Element of L,
O, O1, O2, O3, O4 for Ordinal,
T for T-Sequence;

canceled;

theorem :: KNASTER:16
(f, {})+.x = x;

theorem :: KNASTER:17
(f, {})-.x = x;

theorem :: KNASTER:18
(f, succ O)+.x = f.(f, O)+.x;

theorem :: KNASTER:19
(f, succ O)-.x = f.(f, O)-.x;

theorem :: KNASTER:20
O <> {} & O is_limit_ordinal & dom T = O &
(for A being Ordinal st A in O holds T.A = (f, A)+.x)
implies (f, O)+.x = "\/"(rng T, L);

theorem :: KNASTER:21
O <> {} & O is_limit_ordinal & dom T = O &
(for A being Ordinal st A in O holds T.A = (f, A)-.x)
implies (f, O)-.x = "/\"(rng T, L);

theorem :: KNASTER:22
iter(f, n).x = (f, n)+.x;

theorem :: KNASTER:23
iter(f, n).x = (f, n)-.x;

definition
let L be Lattice, f be (UnOp of the carrier of L),
a be Element of L, O be Ordinal;
redefine func (f, O)+.a -> Element of L;
end;

definition
let L be Lattice, f be (UnOp of the carrier of L),
a be Element of L, O be Ordinal;
redefine func (f, O)-.a -> Element of L;
end;

definition
let L be non empty LattStr, P be Subset of L;
attr P is with_suprema means
:: KNASTER:def 8

for x,y being Element of L st x in P & y in P
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
:: KNASTER:def 9

for x,y being Element of L st x in P & y in P
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;

definition
let L be Lattice;
cluster non empty with_suprema with_infima Subset of L;
end;

definition
let L be Lattice,
P be non empty with_suprema with_infima Subset of L;
func latt P -> strict Lattice means
:: 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 iff x' [= y');
end;

begin :: Complete lattices ::::::::::::::::::::::::::::::::::::::::::::::::

definition
cluster complete -> bounded Lattice;
end;

reserve L for complete Lattice,
f for (monotone UnOp of L),
a, b for Element of L;

theorem :: KNASTER:24
ex a st a is_a_fixpoint_of f;

theorem :: KNASTER:25
for a st a [= f.a for O holds a [= (f, O)+.a;

theorem :: KNASTER:26
for a st f.a [= a for O holds (f, O)-.a [= a;

theorem :: KNASTER:27
for a st a [= f.a
for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a;

theorem :: KNASTER:28
for a st f.a [= a
for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a;

theorem :: KNASTER:29
for a st a [= f.a
for O1, O2 st O1 c< O2 & not (f, O2)+.a is_a_fixpoint_of f
holds (f, O1)+.a <> (f, O2)+.a;

theorem :: KNASTER:30
for a st f.a [= a
for O1, O2 st O1 c< O2 & not (f, O2)-.a is_a_fixpoint_of f
holds (f, O1)-.a <> (f, O2)-.a;

theorem :: KNASTER:31
a [= f.a & (f, O1)+.a is_a_fixpoint_of f implies
for O2 st O1 c= O2 holds (f, O1)+.a = (f, O2)+.a;

theorem :: KNASTER:32
f.a [= a & (f, O1)-.a is_a_fixpoint_of f implies
for O2 st O1 c= O2 holds (f, O1)-.a = (f, O2)-.a;

theorem :: KNASTER:33
for a st a [= f.a
ex O st Card O <=` Card the carrier of L & (f, O)+.a is_a_fixpoint_of f;

theorem :: KNASTER:34
for a st f.a [= a
ex O st Card O <=` Card the carrier of L & (f, O)-.a is_a_fixpoint_of f;

theorem :: KNASTER:35
for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
ex O st Card O <=` Card the carrier of L &
(f, O)+.(a"\/"b) is_a_fixpoint_of f &
a [= (f, O)+.(a"\/"b) & b [= (f, O)+.(a"\/"b);

theorem :: KNASTER:36
for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
ex O st Card O <=` Card the carrier of L &
(f, O)-.(a"/\"b) is_a_fixpoint_of f &
(f, O)-.(a"/\"b) [= a & (f, O)-.(a"/\"b) [= b;

theorem :: KNASTER:37
a [= f.a & a [= b & b is_a_fixpoint_of f
implies for O2 holds (f, O2)+.a [= b;

theorem :: KNASTER:38
f.a [= a & b [= a & b is_a_fixpoint_of f
implies for O2 holds b [= (f, O2)-.a;

definition
let L be complete Lattice, f be UnOp of L such that
f is monotone;
func FixPoints f -> strict Lattice means
:: 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;
end;

theorem :: KNASTER:39
the carrier of FixPoints f = {x where x is Element of L: x is_a_fixpoint_of f}
;

theorem :: KNASTER:40
the carrier of FixPoints f c= the carrier of L;

theorem :: KNASTER:41
(a in the carrier of FixPoints f iff a is_a_fixpoint_of f);

theorem :: KNASTER:42
for x, y being Element of FixPoints f, a, b
st x = a & y = b holds (x [= y iff a [= b);

theorem :: KNASTER:43
FixPoints f is complete;

definition
let L, f;
func lfp f -> Element of L equals
:: KNASTER:def 12
(f, nextcard the carrier of L)+.Bottom L;
func gfp f -> Element of L equals
:: KNASTER:def 13
(f, nextcard the carrier of L)-.Top L;
end;

theorem :: KNASTER:44
(lfp f is_a_fixpoint_of f) &
(ex O st Card O <=` Card the carrier of L & (f, O)+.Bottom L = lfp f);

theorem :: KNASTER:45
(gfp f is_a_fixpoint_of f) &
(ex O st Card O <=` Card the carrier of L & (f, O)-.Top L = gfp f);

theorem :: KNASTER:46
a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f;

theorem :: KNASTER:47
f.a [= a implies lfp f [= a;

theorem :: KNASTER:48
a [= f.a implies a [= gfp f;

begin :: Boolean Lattices

reserve f for (monotone UnOp of BooleLatt A);

definition
let A be set;
cluster BooleLatt A -> complete;
end;

theorem :: KNASTER:49
for f being UnOp of BooleLatt A
holds f is monotone iff f is c=-monotone;

theorem :: KNASTER:50
ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f;

theorem :: KNASTER:51
ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f;
```

Back to top