:: Fix-points in complete lattices
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 16, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, XBOOLE_0, RELAT_1, FUNCT_4, SUBSET_1, NUMBERS, ABIAN,
FUNCT_7, ARYTM_3, COHSP_1, TARSKI, FUNCOP_1, ZFMISC_1, SETFAM_1, FUNCT_2,
LATTICES, STRUCT_0, ORDINAL1, ORDINAL2, EQREL_1, CARD_1, BINOP_1,
LATTICE3, PBOOLE, FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1,
ORDERS_2, XXREAL_0, REWRITE1, XXREAL_2, SEQM_3, KNASTER, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, RELAT_2, ORDERS_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, SETFAM_1, FUNCT_4, WELLORD1, ORDINAL2,
STRUCT_0, COHSP_1, LATTICES, LATTICE3, QUANTAL1, ORDERS_2, ABIAN;
constructors WELLORD1, WELLORD2, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, ABIAN,
BOOLEALG, QUANTAL1, COHSP_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, CARD_1,
STRUCT_0, LATTICES, LATTICE3, QUANTAL1;
requirements NUMERALS, BOOLE, SUBSET;
begin :: Preliminaries
reserve f, g, h for Function;
theorem :: KNASTER:1
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
reserve x, y, z, u, X for set,
A for non empty set,
n for Element of NAT,
f for Function of X, X;
theorem :: KNASTER:2
x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f, n);
theorem :: KNASTER:3
(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 1
for x, y being Element of A st x c= y holds f.x c= f.y;
end;
registration
let A be set, B be non empty set;
cluster c=-monotone for 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 2
meet {h where h is Subset of X : f.h c= h};
func gfp (X, f) -> Subset of X equals
:: KNASTER:def 3
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:4
lfp(X, f) is_a_fixpoint_of f;
theorem :: KNASTER:5
gfp(X, f) is_a_fixpoint_of f;
theorem :: KNASTER:6
f.S c= S implies lfp(X,f) c= S;
theorem :: KNASTER:7
S c= f.S implies S c= gfp(X,f);
theorem :: KNASTER:8
S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f);
::$N Knaster Theorem
scheme :: KNASTER:sch 1
Knaster{A() -> set, F(object) -> 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;
:: Banach decomposition
theorem :: KNASTER:9
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;
::$N Schroeder Bernstein theorem
theorem :: KNASTER:10
for X, Y being non empty set,
f being Function of X, Y,
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;
theorem :: KNASTER:11 ::: EULER_1:12
f is bijective implies X,Y are_equipotent;
theorem :: KNASTER:12
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 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 -> set means
:: 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);
func (f, O)-.x -> set means
:: 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);
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 Sequence;
theorem :: KNASTER:13
(f, 0)+.x = x;
theorem :: KNASTER:14
(f, 0)-.x = x;
theorem :: KNASTER:15
(f, succ O)+.x = f.(f, O)+.x;
theorem :: KNASTER:16
(f, succ O)-.x = f.(f, O)-.x;
theorem :: KNASTER:17
O <> 0 & 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:18
O <> 0 & 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:19
iter(f, n).x = (f, n)+.x;
theorem :: KNASTER:20
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 6
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 z9 being Element
of L st z9 in P & x [= z9 & y [= z9 holds z [= z9;
attr P is with_infima means
:: KNASTER:def 7
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 z9 being Element
of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z;
end;
registration
let L be Lattice;
cluster non empty with_suprema with_infima for 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 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
iff x9 [= y9);
end;
begin :: Complete lattices
registration
cluster complete -> bounded for Lattice;
end;
reserve L for complete Lattice,
f for monotone UnOp of L,
a, b for Element of L;
theorem :: KNASTER:21
ex a st a is_a_fixpoint_of f;
theorem :: KNASTER:22
for a st a [= f.a for O holds a [= (f, O)+.a;
theorem :: KNASTER:23
for a st f.a [= a for O holds (f, O)-.a [= a;
theorem :: KNASTER:24
for a st a [= f.a for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a;
theorem :: KNASTER:25
for a st f.a [= a for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a;
theorem :: KNASTER:26
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:27
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:28
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:29
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:30
for a st a [= f.a ex O st card O c= card the carrier of L & (f,
O)+.a is_a_fixpoint_of f;
theorem :: KNASTER:31
for a st f.a [= a ex O st card O c= card the carrier of L & (f,
O)-.a is_a_fixpoint_of f;
theorem :: KNASTER:32
for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O 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);
theorem :: KNASTER:33
for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O 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;
theorem :: KNASTER:34
a [= b & b is_a_fixpoint_of f implies for O2 holds (f, O2)+.a [= b;
theorem :: KNASTER:35
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 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;
end;
theorem :: KNASTER:36
the carrier of FixPoints f = {x where x is Element of L: x
is_a_fixpoint_of f};
theorem :: KNASTER:37
the carrier of FixPoints f c= the carrier of L;
theorem :: KNASTER:38
a in the carrier of FixPoints f iff a is_a_fixpoint_of f;
theorem :: KNASTER:39
for x, y being Element of FixPoints f, a, b st x = a & y = b
holds (x [= y iff a [= b);
theorem :: KNASTER:40
FixPoints f is complete;
definition
let L, f;
func lfp f -> Element of L equals
:: KNASTER:def 10
(f, nextcard the carrier of L)+.Bottom L;
func gfp f -> Element of L equals
:: KNASTER:def 11
(f, nextcard the carrier of L)-.Top L;
end;
theorem :: KNASTER:41
lfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
L & (f, O)+.Bottom L = lfp f;
theorem :: KNASTER:42
gfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
L & (f, O)-.Top L = gfp f;
theorem :: KNASTER:43
a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f;
theorem :: KNASTER:44
f.a [= a implies lfp f [= a;
theorem :: KNASTER:45
a [= f.a implies a [= gfp f;
begin :: Boolean Lattices
reserve f for monotone UnOp of BooleLatt A;
theorem :: KNASTER:46
for f being UnOp of BooleLatt A holds f is monotone iff f is c=-monotone;
theorem :: KNASTER:47
ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f;
theorem :: KNASTER:48
ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f;