:: Fix-points in complete lattices
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 16, 1996
:: Copyright (c) 1996-2026 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;
definitions TARSKI, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0, ABIAN;
equalities RELAT_1, LATTICE3, WELLORD1, ORDINAL1;
expansions TARSKI, RELAT_1, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0,
ABIAN;
theorems TARSKI, SETFAM_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_2,
FUNCT_4, CARD_1, COHSP_1, LATTICES, LATTICE3, QUANTAL1, FILTER_0,
FILTER_1, BOOLEALG, WELLORD1, RELSET_1, ORDERS_2, RELAT_2, ORDINAL1,
CARD_3, XBOOLE_0, XBOOLE_1, FUNCT_7, PARTFUN1, ORDERS_1, NAT_1, XTUPLE_0;
schemes NAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, ORDINAL2;
begin :: Preliminaries
reserve f, g, h for Function;
theorem
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)
proof
assume that
A1: h = f \/ g and
A2: dom f misses dom g;
A3: dom h = dom f \/ dom g by A1,XTUPLE_0:23;
hereby
assume
A4: h is one-to-one;
thus f is one-to-one
proof
assume not f is one-to-one;
then consider x1, x2 being object such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2 & x1<>x2;
A8: x2 in dom h by A3,A6,XBOOLE_0:def 3;
[x2, f.x2] in f by A6,FUNCT_1:def 2;
then [x2, f.x2] in h by A1,XBOOLE_0:def 3;
then
A9: f.x2 = h.x2 by A8,FUNCT_1:def 2;
A10: x1 in dom h by A3,A5,XBOOLE_0:def 3;
[x1, f.x1] in f by A5,FUNCT_1:def 2;
then [x1, f.x1] in h by A1,XBOOLE_0:def 3;
then f.x1 = h.x1 by A10,FUNCT_1:def 2;
hence contradiction by A4,A7,A10,A8,A9;
end;
thus g is one-to-one
proof
assume not g is one-to-one;
then consider x1, x2 being object such that
A11: x1 in dom g and
A12: x2 in dom g and
A13: g.x1 = g.x2 & x1<>x2;
A14: x2 in dom h by A3,A12,XBOOLE_0:def 3;
[x2, g.x2] in g by A12,FUNCT_1:def 2;
then [x2, g.x2] in h by A1,XBOOLE_0:def 3;
then
A15: g.x2 = h.x2 by A14,FUNCT_1:def 2;
A16: x1 in dom h by A3,A11,XBOOLE_0:def 3;
[x1, g.x1] in g by A11,FUNCT_1:def 2;
then [x1, g.x1] in h by A1,XBOOLE_0:def 3;
then g.x1 = h.x1 by A16,FUNCT_1:def 2;
hence contradiction by A4,A13,A16,A14,A15;
end;
thus rng f misses rng g
proof
assume not thesis;
then consider hx being object such that
A17: hx in rng f and
A18: hx in rng g by XBOOLE_0:3;
consider x1 being object such that
A19: x1 in dom f and
A20: hx = f.x1 by A17,FUNCT_1:def 3;
A21: x1 in dom h by A3,A19,XBOOLE_0:def 3;
consider x2 being object such that
A22: x2 in dom g and
A23: hx = g.x2 by A18,FUNCT_1:def 3;
A24: x2 in dom h by A3,A22,XBOOLE_0:def 3;
A25: hx is set by TARSKI:1;
[x2, hx] in g by A22,A23,FUNCT_1:def 2;
then [x2, hx] in h by A1,XBOOLE_0:def 3;
then
A26: h.x2 = hx by A24,FUNCT_1:def 2,A25;
A27: x1 <> x2 by A2,A19,A22,XBOOLE_0:3;
[x1, hx] in f by A19,A20,FUNCT_1:def 2;
then [x1, hx] in h by A1,XBOOLE_0:def 3;
then h.x1 = hx by A21,FUNCT_1:def 2,A25;
hence contradiction by A4,A27,A21,A24,A26;
end;
end;
assume
A28: f is one-to-one & g is one-to-one & rng f misses rng g;
f \/ g = f+*g by A2,FUNCT_4:31;
hence thesis by A1,A28,FUNCT_4:92;
end;
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 Th2:
x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f, n)
proof
assume
A1: x is_a_fixpoint_of iter(f,n);
then
A2: x in dom iter(f, n);
A3: dom f = X by FUNCT_2:52;
then dom iter(f, n) = X & f.x in rng f by A2,FUNCT_1:def 3,FUNCT_2:52;
hence f.x in dom iter(f, n);
x = iter(f, n).x by A1;
hence f.x = (f*iter(f, n)).x by A2,FUNCT_1:13
.= iter(f, n+1).x by FUNCT_7:71
.= (iter(f, n)*f).x by FUNCT_7:69
.= iter(f, n).(f.x) by A2,A3,FUNCT_1:13;
end;
theorem
(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
proof
given n such that
A1: x is_a_fixpoint_of iter(f, n) and
A2: for y st y is_a_fixpoint_of iter(f,n) holds x = y;
dom f = X & dom iter(f, n) = X by FUNCT_2:52;
hence x in dom f by A1;
thus thesis by A1,A2,Th2;
end;
definition
let A, B be non empty set, f be Function of A, B;
redefine attr f is c=-monotone means :: redefines c=-monotone (COHSP_1, definition)
:Def1:
for x, y being Element of A st x c= y holds f.x c= f.y;
compatibility
proof
dom f = A by FUNCT_2:def 1;
hence f is c=-monotone implies for x, y being Element of A st x c= y holds
f.x c= f.y;
assume
A1: for x, y being Element of A st x c= y holds f.x c= f.y;
let x, y be set;
assume x in dom f & y in dom f & x c= y;
hence thesis by A1;
end;
end;
registration
let A be set, B be non empty set;
cluster c=-monotone for Function of A, B;
existence
proof
set b = the Element of B;
reconsider f = A --> b as Function of A, B;
take f;
let x, y be set;
assume that
A1: x in dom f and
A2: y in dom f and
x c= y;
f.x = b by A1,FUNCOP_1:7
.= f.y by A2,FUNCOP_1:7;
hence thesis;
end;
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
meet {h where h is Subset of X : f.h c= h};
coherence
proof
defpred P[set] means f.$1 c= $1;
reconsider H = {h where h is Subset of X : P[h] } as Subset-Family of X
from DOMAIN_1:sch 7;
reconsider H as Subset-Family of X;
meet H is Subset of X;
hence thesis;
end;
func gfp (X, f) -> Subset of X equals
union {h where h is Subset of X : h c= f.h };
coherence
proof
defpred P[set] means $1 c= f.$1;
reconsider H = {h where h is Subset of X : P[h] } as Subset-Family of X
from DOMAIN_1:sch 7;
union H is Subset of X;
hence thesis;
end;
end;
reserve f for c=-monotone Function of bool X, bool X,
S for Subset of X;
theorem Th4:
lfp(X, f) is_a_fixpoint_of f
proof
defpred P[set] means f.$1 c= $1;
reconsider H = { h where h is Subset of X : P[h] } as Subset-Family of X
from DOMAIN_1:sch 7;
reconsider H as Subset-Family of X;
set A = meet H;
now
X c= X;
then reconsider X9 = X as Subset of X;
f.X9 c= X9;
then X9 in H;
hence H <> {};
let h be set;
assume
A1: h in H;
then consider x being Subset of X such that
A2: x = h and
A3: f.x c= x;
A c= h by A1,SETFAM_1:3;
then f.A c= f.x by A2,Def1;
hence f.A c= h by A2,A3;
end;
then
A4: f.A c= A by SETFAM_1:5;
then f.(f.A) c= f.A by Def1;
then f.A in H;
then A c= f.A by SETFAM_1:3;
hence f.(lfp(X,f)) = lfp(X,f) by A4;
end;
theorem Th5:
gfp(X, f) is_a_fixpoint_of f
proof
defpred P[set] means $1 c= f.$1;
reconsider H = { h where h is Subset of X : P[h] } as Subset-Family of X
from DOMAIN_1:sch 7;
set A = union H;
now
let x be set;
assume
A1: x in H;
then consider h being Subset of X such that
A2: x = h and
A3: h c= f.h;
h c= A by A1,A2,ZFMISC_1:74;
then f.h c= f.A by Def1;
hence x c= f.A by A2,A3;
end;
then
A4: A c= f.A by ZFMISC_1:76;
then f.A c= f.(f.A) by Def1;
then f.A in H;
then f.A c= A by ZFMISC_1:74;
hence f.(gfp (X,f)) = gfp(X,f) by A4;
end;
theorem Th6:
f.S c= S implies lfp(X,f) c= S
proof
set H = {h where h is Subset of X : f.h c= h };
assume f.S c= S;
then S in H;
hence thesis by SETFAM_1:3;
end;
theorem Th7:
S c= f.S implies S c= gfp(X,f)
proof
set H = {h where h is Subset of X : h c= f.h };
assume S c= f.S;
then S in H;
hence thesis by ZFMISC_1:74;
end;
theorem Th8:
S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f) by Th6,Th7;
::$N Knaster Theorem
::$L https://en.wikipedia.org/wiki/KnasterâTarski_theorem Knaster Theorem
scheme
Knaster{A() -> set, F(object) -> set}:
ex D being set st F(D) = D & D c= A()
provided
A1: for X, Y being set st X c= Y holds F(X) c= F(Y) and
A2: F(A()) c= A()
proof
consider f being Function such that
A3: dom f = bool A() & for x being object st x in bool A() holds f.x = F(x)
from FUNCT_1:sch 3;
rng f c= bool A()
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: x = f.y by FUNCT_1:def 3;
F(y) c= F(A()) by A1,A3,A4;
then F(y) c= A() by A2;
then f.y c= A() by A3,A4;
hence thesis by A5;
end;
then reconsider f as Function of bool A(), bool A() by A3,FUNCT_2:def 1
,RELSET_1:4;
now
let a, b be set;
assume that
A6: a in dom f & b in dom f and
A7: a c= b;
f.a = F(a) & f.b = F(b) by A3,A6;
hence f.a c= f.b by A1,A7;
end;
then reconsider f as c=-monotone Function of bool A(), bool A() by
COHSP_1:def 11;
take d = lfp(A(), f);
d is_a_fixpoint_of f by Th4;
then d = f.d;
hence F(d) = d by A3;
thus thesis;
end;
reserve X, Y for non empty set,
f for Function of X, Y,
g for Function of Y, X;
:: Banach decomposition
theorem Th9:
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
deffunc F(set)= X\g.:(Y\f.:$1);
A1: for x being set st x in bool X holds F(x) in bool X;
consider h being Function of bool X, bool X such that
A2: for x being set st x in bool X holds h.x =F(x) from FUNCT_2:sch 11(A1);
now
let x, y be set;
assume that
A3: x in dom h and
A4: y in dom h and
A5: x c= y;
f.:x c= f.:y by A5,RELAT_1:123;
then Y \ f.:y c= Y \ f.:x by XBOOLE_1:34;
then g.:(Y \ f.:y) c= g.:(Y \ f.:x) by RELAT_1:123;
then X \ g.:(Y \ f.:x) c= X \ g.:(Y \ f.:y) by XBOOLE_1:34;
then h.x c= X \ g.:(Y \ f.:y) by A2,A3;
hence h.x c= h.y by A2,A4;
end;
then reconsider h as c=-monotone Function of bool X, bool X by COHSP_1:def 11
;
take Xa = lfp (X, h);
take Xb = X \ Xa;
take Ya = f.:Xa;
take Yb = Y \ Ya;
thus Xa misses Xb by XBOOLE_1:79;
thus Ya misses Yb by XBOOLE_1:79;
thus Xa \/ Xb = X by XBOOLE_1:45;
thus Ya \/ Yb = Y by XBOOLE_1:45;
thus f.:Xa = Ya;
A6: Xa is_a_fixpoint_of h by Th4;
thus g.:Yb = X/\g.:(Y\f.:Xa) by XBOOLE_1:28
.= X\(X\g.:(Y\f.:Xa)) by XBOOLE_1:48
.= X\h.Xa by A2
.= Xb by A6;
end;
::$N Schroeder Bernstein theorem
::$L https://en.wikipedia.org/wiki/SchröderâBernstein_theorem Schroeder Bernstein theorem
theorem Th10:
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
proof
let X, Y be non empty set,
f be Function of X, Y,
g be Function of Y, X;
assume that
A1: f is one-to-one and
A2: g is one-to-one;
consider Xa, Xb, Ya, Yb being set such that
A3: Xa misses Xb and
A4: Ya misses Yb and
A5: Xa \/ Xb = X and
A6: Ya \/ Yb = Y and
A7: f.:Xa = Ya and
A8: g.:Yb = Xb by Th9;
set gYb = g|Yb;
A9: gYb is one-to-one by A2,FUNCT_1:52;
set fXa = f|Xa;
dom f = X by FUNCT_2:def 1;
then
A10: dom fXa = Xa by A5,RELAT_1:62,XBOOLE_1:7;
set h = fXa+*gYb";
rng gYb = Xb by A8,RELAT_1:115;
then
A11: dom (gYb") = Xb by A9,FUNCT_1:32;
then
A12: X = dom h by A5,A10,FUNCT_4:def 1;
A13: rng fXa = Ya by A7,RELAT_1:115;
dom g = Y by FUNCT_2:def 1;
then dom gYb = Yb by A6,RELAT_1:62,XBOOLE_1:7;
then
A14: rng (gYb") = Yb by A9,FUNCT_1:33;
fXa \/ gYb" = h by A3,A10,A11,FUNCT_4:31;
then
A15: rng h = Y by A6,A13,A14,RELAT_1:12;
then reconsider h as Function of X, Y by A12,FUNCT_2:def 1,RELSET_1:4;
A16: h is onto by A15,FUNCT_2:def 3;
take h;
fXa is one-to-one by A1,FUNCT_1:52;
then h is one-to-one by A4,A13,A9,A14,FUNCT_4:92;
hence thesis by A16,FUNCT_2:def 4;
end;
theorem Th11: ::: EULER_1:12
f is bijective implies X,Y are_equipotent
proof
assume
A1: f is bijective;
take h = f;
A2: h is one-to-one onto by A1,FUNCT_2:def 4;
then
A3: rng h = Y by FUNCT_2:def 3;
hereby
let x be object;
assume
A4: x in X;
reconsider y = h.x as object;
take y;
thus y in Y by A3,A4,FUNCT_2:4;
x in dom h by A4,FUNCT_2:def 1;
hence [x,y] in h by FUNCT_1:1;
end;
hereby
let y be object;
assume y in Y;
then consider x being object such that
A5: x in dom h & y = h.x by A3,FUNCT_1:def 3;
reconsider x as object;
take x;
thus x in X & [x,y] in h by A5,FUNCT_1:1;
end;
let x,y,z,u be object;
assume that
A6: [x,y] in h and
A7: [z,u] in h;
A8: z in dom h & u = h.z by A7,FUNCT_1:1;
x in dom h & y = h.x by A6,FUNCT_1:1;
hence thesis by A2,A8;
end;
theorem
f is one-to-one & g is one-to-one implies X,Y are_equipotent
proof
assume f is one-to-one & g is one-to-one;
then ex h being Function of X,Y st h is bijective by Th10;
hence thesis by Th11;
end;
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
:Def4:
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
proof
deffunc D(Ordinal,Sequence)="\/"(rng $2, L);
deffunc C(Ordinal,set)=f.$2;
(ex z being object,S being Sequence
st z = last S & dom S = succ O & S.0 = x
& (for C being Ordinal st succ C in succ O holds S.succ C = C(C,S.C)) &
for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds S.C = D
(C,S|C) ) & for x1,x2 being set st (ex L0 being Sequence st x1 = last L0 &
dom L0 = succ O & L0.0 = x & (for C being Ordinal st succ C in succ O holds L0
.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C is
limit_ordinal holds L0.C = D(C,L0|C) ) & (ex L0 being Sequence st x2 = last
L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal st succ C in succ O
holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C
is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
func (f, O)-.x -> set means
:Def5:
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
proof
deffunc D(Ordinal,Sequence)="/\"(rng $2, L);
deffunc C(Ordinal,set)=f.$2;
(ex z being object,S being Sequence st z = last S & dom S = succ O & S.
0 = x & (for C being Ordinal st succ C in succ O holds S.succ C = C(C,S.C)) &
for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds S.C = D
(C,S|C) ) & for x1,x2 being set st (ex L0 being Sequence st x1 = last L0 &
dom L0 = succ O & L0.0 = x & (for C being Ordinal st succ C in succ O holds L0
.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C is
limit_ordinal holds L0.C = D(C,L0|C) ) & (ex L0 being Sequence st x2 = last
L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal st succ C in succ O
holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C
is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
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 Th13:
(f, 0)+.x = x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
A1: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
thus F(0) = x from ORDINAL2:sch 8(A1);
end;
theorem Th14:
(f, 0)-.x = x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
A1: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
thus F(0) = x from ORDINAL2:sch 8(A1);
end;
theorem Th15:
(f, succ O)+.x = f.(f, O)+.x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
A1: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
hence thesis;
end;
theorem Th16:
(f, succ O)-.x = f.(f, O)-.x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
A1: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
hence thesis;
end;
theorem Th17:
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)
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
assume that
A1: O <> 0 & O is limit_ordinal and
A2: dom T = O and
A3: for A being Ordinal st A in O holds T.A = F(A);
A4: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
thus F(O) = D(O,T) from ORDINAL2:sch 10(A4, A1, A2, A3);
end;
theorem Th18:
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)
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
assume that
A1: O <> 0 & O is limit_ordinal and
A2: dom T = O and
A3: for A being Ordinal st A in O holds T.A = F(A);
A4: for O being Ordinal, y being object holds y = F(O) iff ex L0 being
Sequence st y = last L0 & dom L0 = succ O & L0.0 = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
thus F(O) = D(O,T) from ORDINAL2:sch 10(A4, A1, A2, A3);
end;
theorem
iter(f, n).x = (f, n)+.x
proof
defpred P[Nat] means iter(f, $1).x = (f, $1)+.x;
A1: dom f = the carrier of L by FUNCT_2:def 1;
then
A2: x in field f by XBOOLE_0:def 3;
A3: now
let n be Nat;
assume
A4: P[n];
rng f c= the carrier of L;
then
A5: dom iter(f, n) = dom f by A1,FUNCT_7:74;
iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:71
.= f.(f, n)+.x by A1,A4,A5,FUNCT_1:13
.= (f, succ Segm n)+.x by Th15
.= (f, Segm(n+1))+.x by NAT_1:38;
hence P[n+1];
end;
iter(f, 0).x = id(field f).x by FUNCT_7:68
.= x by A2,FUNCT_1:18
.= (f, 0)+.x by Th13;
then
A6: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A6, A3);
hence thesis;
end;
theorem
iter(f, n).x = (f, n)-.x
proof
defpred P[Nat] means iter(f, $1).x = (f, $1)-.x;
A1: dom f = the carrier of L by FUNCT_2:def 1;
then
A2: x in field f by XBOOLE_0:def 3;
A3: now
let n be Nat;
assume
A4: P[n];
rng f c= the carrier of L;
then
A5: dom iter(f, n) = dom f by A1,FUNCT_7:74;
iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:71
.= f.(f, n)-.x by A1,A4,A5,FUNCT_1:13
.= (f, succ Segm n)-.x by Th16
.= (f, Segm(n+1))-.x by NAT_1:38;
hence P[n+1];
end;
iter(f, 0).x = id(field f).x by FUNCT_7:68
.= x by A2,FUNCT_1:18
.= (f, 0)-.x by Th14;
then
A6: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A6, A3);
hence thesis;
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; :: redefines +. (KNASTER, definition)
coherence
proof
deffunc F(Ordinal)=(f, $1)+.a;
defpred P[Ordinal] means (f, $1)+.a is Element of L;
A1: now
let O1;
assume P[O1];
then reconsider fa = (f, O1)+.a as Element of L;
f.fa = (f, succ O1)+.a by Th15;
hence P[succ O1];
end;
A2: now
let O1;
assume that
A3: O1 <> 0 & O1 is limit_ordinal and
for O2 st O2 in O1 holds P[O2];
consider Ls being Sequence such that
A4: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(
O2) from ORDINAL2:sch 2;
(f, O1)+.a = "\/"(rng Ls, L) by A3,A4,Th17;
hence P[O1];
end;
A5: P[0] by Th13;
for O holds P[O] from ORDINAL2:sch 1(A5, A1, A2);
hence thesis;
end;
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; :: redefines -. (KNASTER, definition)
coherence
proof
deffunc F(Ordinal)=(f, $1)-.a;
defpred P[Ordinal] means (f, $1)-.a is Element of L;
A1: now
let O1;
assume P[O1];
then reconsider fa = (f, O1)-.a as Element of L;
f.fa = (f, succ O1)-.a by Th16;
hence P[succ O1];
end;
A2: now
let O1;
assume that
A3: O1 <> 0 & O1 is limit_ordinal and
for O2 st O2 in O1 holds P[O2];
consider Ls being Sequence such that
A4: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 =F(O2
) from ORDINAL2:sch 2;
(f, O1)-.a = "/\"(rng Ls, L) by A3,A4,Th18;
hence P[O1];
end;
A5: P[0] by Th14;
for O holds P[O] from ORDINAL2:sch 1(A5, A1, A2);
hence thesis;
end;
end;
definition
let L be non empty LattStr, P be Subset of L;
attr P is with_suprema means
:Def6:
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
:Def7:
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;
existence
proof
the carrier of L c= the carrier of L;
then reconsider P = the carrier of L as Subset of L;
take P;
thus P is non empty;
thus P is with_suprema
proof
let x,y be Element of L such that
x in P and
y in P;
take z = x"\/"y;
thus z in P;
thus x [= z & y [= z by LATTICES:5;
let z9 be Element of L;
assume that
z9 in P and
A1: x [= z9 & y [= z9;
thus z [= z9 by A1,BOOLEALG:5;
end;
let x,y be Element of L such that
x in P and
y in P;
take z = x"/\"y;
thus z in P;
thus z [= x & z [= y by LATTICES:6;
let z9 be Element of L;
assume that
z9 in P and
A2: z9 [= x & z9 [= y;
thus z9 [= z by A2,BOOLEALG:6;
end;
end;
definition
let L be Lattice, P be non empty with_suprema with_infima Subset of L;
func latt P -> strict Lattice means
:Def8:
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);
existence
proof
set cL = the carrier of L;
set LL = LattRel L;
set LR = LL|_2 P;
reconsider LR as Relation of P by XBOOLE_1:17;
field LL = cL by FILTER_1:32;
then
A1: LL is_reflexive_in cL by RELAT_2:def 9;
A2: field LR = P
proof
thus field LR c= P by WELLORD1:13;
let x be object;
assume x in P;
then [x,x] in [:P, P:] & [x,x] in LL by A1,RELAT_2:def 1,ZFMISC_1:87;
then [x, x] in LR by XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
LR is reflexive by WELLORD1:15;
then
A3: LR is_reflexive_in P by A2,RELAT_2:def 9;
then
A4: dom LR = P by ORDERS_1:13;
LR is transitive by WELLORD1:17;
then
A5: LR is_transitive_in P by A2,RELAT_2:def 16;
LR is antisymmetric by WELLORD1:18;
then
A6: LR is_antisymmetric_in P by A2,RELAT_2:def 12;
reconsider LR as Order of P by A4,PARTFUN1:def 2,WELLORD1:15,17,18;
set RS = RelStr(#P, LR#);
take IT = latt RS;
A7: RS is with_suprema
proof
let x,y be Element of RS;
x in P & y in P;
then reconsider xL = x, yL = y as Element of L;
consider zL being Element of L such that
A8: zL in P and
A9: xL [= zL and
A10: yL [= zL and
A11: for z9 being Element of L st z9 in P & xL [= z9 & yL [= z9
holds zL [= z9 by Def6;
[yL,zL] in [:P,P:] & [yL,zL] in LL by A8,A10,FILTER_1:31,ZFMISC_1:87;
then
A12: [yL,zL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of RS by A8;
take z;
[xL,zL] in [:P,P:] & [xL,zL] in LL by A8,A9,FILTER_1:31,ZFMISC_1:87;
then [xL,zL] in LR by XBOOLE_0:def 4;
hence x <= z & y <= z by A12,ORDERS_2:def 5;
let z9 be Element of RS;
assume that
A13: x <= z9 and
A14: y <= z9;
z9 in P;
then reconsider z9L = z9 as Element of L;
[y,z9] in LR by A14,ORDERS_2:def 5;
then [y,z9] in LL by XBOOLE_0:def 4;
then
A15: yL [= z9L by FILTER_1:31;
[x,z9] in LR by A13,ORDERS_2:def 5;
then [x,z9] in LL by XBOOLE_0:def 4;
then xL [= z9L by FILTER_1:31;
then zL [= z9L by A11,A15;
then
A16: [zL,z9L] in LL by FILTER_1:31;
[zL,z9L] in [:P, P:] by A8,ZFMISC_1:87;
then [zL,z9L] in LR by A16,XBOOLE_0:def 4;
hence thesis by ORDERS_2:def 5;
end;
A17: RS is with_infima
proof
let x,y be Element of RS;
x in P & y in P;
then reconsider xL = x, yL = y as Element of L;
consider zL being Element of L such that
A18: zL in P and
A19: zL [= xL and
A20: zL [= yL and
A21: for z9 being Element of L st z9 in P & z9 [= xL & z9 [= yL
holds z9 [= zL by Def7;
[zL,yL] in [:P,P:] & [zL,yL] in LL by A18,A20,FILTER_1:31,ZFMISC_1:87;
then
A22: [zL,yL] in LR by XBOOLE_0:def 4;
reconsider z = zL as Element of RS by A18;
take z;
[zL,xL] in [:P,P:] & [zL,xL] in LL by A18,A19,FILTER_1:31,ZFMISC_1:87;
then [zL,xL] in LR by XBOOLE_0:def 4;
hence z <= x & z <= y by A22,ORDERS_2:def 5;
let z9 be Element of RS;
assume that
A23: z9 <= x and
A24: z9 <= y;
z9 in P;
then reconsider z9L = z9 as Element of L;
[z9,y] in LR by A24,ORDERS_2:def 5;
then [z9,y] in LL by XBOOLE_0:def 4;
then
A25: z9L [= yL by FILTER_1:31;
[z9,x] in LR by A23,ORDERS_2:def 5;
then [z9,x] in LL by XBOOLE_0:def 4;
then z9L [= xL by FILTER_1:31;
then z9L [= zL by A21,A25;
then
A26: [z9L,zL] in LL by FILTER_1:31;
[z9L,zL] in [:P, P:] by A18,ZFMISC_1:87;
then [z9L,zL] in LR by A26,XBOOLE_0:def 4;
hence thesis by ORDERS_2:def 5;
end;
A27: RS is Poset by A3,A6,A5,ORDERS_2:def 2,def 3,def 4;
then
A28: RS = LattPOSet IT by A7,A17,LATTICE3:def 15;
LattPOSet IT = RelStr(#the carrier of IT, LattRel IT#);
hence the carrier of IT = P by A7,A17,A27,LATTICE3:def 15;
let x, y be Element of IT;
x in P & y in P by A28;
then reconsider x9 = x, y9 = y as Element of L;
take x9, y9;
thus x = x9 & y = y9;
hereby
assume x [= y;
then [x, y] in LR by A28,FILTER_1:31;
then [x, y] in LattRel L by XBOOLE_0:def 4;
hence x9 [= y9 by FILTER_1:31;
end;
assume x9 [= y9;
then
A29: [x, y] in LattRel L by FILTER_1:31;
[x, y] in [:P, P:] by A28,ZFMISC_1:87;
then [x, y] in LattRel IT by A28,A29,XBOOLE_0:def 4;
hence thesis by FILTER_1:31;
end;
uniqueness
proof
let it1, it2 be strict Lattice such that
A30: the carrier of it1 = P and
A31: for x, y being Element of it1 ex x9, y9 being Element of L st x =
x9 & y = y9 & (x [= y iff x9 [= y9) and
A32: the carrier of it2 = P and
A33: for x, y being Element of it2 ex x9, y9 being Element of L st x =
x9 & y = y9 & (x [= y iff x9 [= y9);
A34: LattRel it2 = { [p,q] where p is Element of it2, q is Element of it2:
p [= q } by FILTER_1:def 8;
A35: LattRel it1 = { [p,q] where p is Element of it1, q is Element of it1:
p [= q } by FILTER_1:def 8;
now
let a be object;
hereby
assume a in LattRel it1;
then consider p1, q1 being Element of it1 such that
A36: a = [p1, q1] & p1 [= q1 by A35;
reconsider p1, q1 as Element of it1;
reconsider p2 = p1, q2 = q1 as Element of it2 by A30,A32;
(ex pl1, ql1 being Element of L st p1 = pl1 & q1 = ql1 &( p1 [=
q1 iff pl1 [= ql1))& ex pl2, ql2 being Element of L st p2 = pl2 & q2 = ql2 &(
p2 [= q2 iff pl2 [= ql2) by A31,A33;
hence a in LattRel it2 by A34,A36;
end;
assume a in LattRel it2;
then consider p1, q1 being Element of it2 such that
A37: a = [p1, q1] & p1 [= q1 by A34;
reconsider p1, q1 as Element of it2;
reconsider p2 = p1, q2 = q1 as Element of it1 by A30,A32;
(ex pl1, ql1 being Element of L st p1 = pl1 & q1 = ql1 &( p1 [= q1
iff pl1 [= ql1))& ex pl2, ql2 being Element of L st p2 = pl2 & q2 = ql2 &( p2
[= q2 iff pl2 [= ql2) by A31,A33;
hence a in LattRel it1 by A35,A37;
end;
then
A38: LattRel it1 = LattRel it2;
LattPOSet it1 = RelStr(#the carrier of it1,LattRel it1#) & LattPOSet
it2 = RelStr(#the carrier of it2,LattRel it2#);
hence thesis by A30,A32,A38,LATTICE3:6;
end;
end;
begin :: Complete lattices
registration
cluster complete -> bounded for Lattice;
coherence
proof
let L be Lattice;
assume L is complete;
then L is 0_Lattice & L is 1_Lattice by LATTICE3:49,50;
hence thesis;
end;
end;
reserve L for complete Lattice,
f for monotone UnOp of L,
a, b for Element of L;
theorem Th21:
ex a st a is_a_fixpoint_of f
proof
set H = {h where h is Element of L: h [= f.h};
set fH = {f.h where h is Element of L: h [= f.h};
set uH = "\/"(H, L);
set fuH = "\/"(fH, L);
take uH;
now
let fh be Element of L;
assume fh in fH;
then consider h being Element of L such that
A1: fh = f.h and
A2: h [= f.h;
h in H by A2;
then h [= uH by LATTICE3:38;
hence fh [= f.uH by A1,QUANTAL1:def 12;
end;
then fH is_less_than f.uH;
then
A3: fuH [= f.uH by LATTICE3:def 21;
now
let a be Element of L;
assume a in H;
then consider h being Element of L such that
A4: a = h & h [= f.h;
reconsider fh = f.h as Element of L;
take fh;
thus a [= fh & fh in fH by A4;
end;
then uH [= fuH by LATTICE3:47;
then
A5: uH [= f.uH by A3,LATTICES:7;
then f.uH [= f.(f.uH) by QUANTAL1:def 12;
then f.uH in H;
then f.uH [= uH by LATTICE3:38;
hence uH = f.uH by A5,LATTICES:8;
end;
theorem Th22:
for a st a [= f.a for O holds a [= (f, O)+.a
proof
let a;
defpred S[Ordinal] means a [= (f, $1)+.a;
deffunc F(Ordinal)=(f, $1)+.a;
A1: now
let O1;
assume that
A2: O1 <> 0 and
A3: O1 is limit_ordinal and
A4: for O2 st O2 in O1 holds S[O2];
consider O2 being object such that
A5: O2 in O1 by A2,XBOOLE_0:def 1;
reconsider O2 as Ordinal by A5;
A6: S[O2] by A4,A5;
consider Ls being Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2
) from ORDINAL2:sch 2;
Ls.O2 = (f, O2)+.a & Ls.O2 in rng Ls by A7,A5,FUNCT_1:def 3;
then (f, O2)+.a [= "\/"(rng Ls, L) by LATTICE3:38;
then a [= "\/"(rng Ls, L) by A6,LATTICES:7;
hence S[O1] by A2,A3,A7,Th17;
end;
assume
A8: a [= f.a;
A9: now
let O1;
assume S[O1];
then f.a [= f.((f, O1)+.a) by QUANTAL1:def 12;
then a [= f.((f, O1)+.a) by A8,LATTICES:7;
hence S[succ O1] by Th15;
end;
A10: S[0] by Th13;
thus for O holds S[O] from ORDINAL2:sch 1(A10, A9, A1);
end;
theorem Th23:
for a st f.a [= a for O holds (f, O)-.a [= a
proof
let a;
defpred S[Ordinal] means (f, $1)-.a [= a;
deffunc F(Ordinal)=(f, $1)-.a;
A1: now
let O1;
assume that
A2: O1 <> 0 and
A3: O1 is limit_ordinal and
A4: for O2 st O2 in O1 holds S[O2];
consider O2 being object such that
A5: O2 in O1 by A2,XBOOLE_0:def 1;
reconsider O2 as Ordinal by A5;
A6: S[O2] by A4,A5;
consider Ls being Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2
) from ORDINAL2:sch 2;
Ls.O2 = (f, O2)-.a & Ls.O2 in rng Ls by A7,A5,FUNCT_1:def 3;
then "/\"(rng Ls, L) [= (f, O2)-.a by LATTICE3:38;
then "/\"(rng Ls, L) [= a by A6,LATTICES:7;
hence S[O1] by A2,A3,A7,Th18;
end;
assume
A8: f.a [= a;
A9: now
let O1;
assume S[O1];
then f.((f, O1)-.a) [= f.a by QUANTAL1:def 12;
then f.((f, O1)-.a) [= a by A8,LATTICES:7;
hence S[succ O1] by Th16;
end;
A10: S[0] by Th14;
thus for O holds S[O] from ORDINAL2:sch 1(A10, A9, A1);
end;
theorem Th24:
for a st a [= f.a for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a
proof
let a;
defpred S[Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O1)+.a
[= (f, O2)+.a;
A1: now
let O4;
assume that
A2: O4 <> 0 & O4 is limit_ordinal and
A3: for O3 st O3 in O4 holds S[O3];
thus S[O4]
proof
let O1, O2;
assume that
A4: O1 c= O2 and
A5: O2 c= O4;
A6: O2 c< O4 iff O2 c= O4 & O2 <> O4;
A7: O1 c< O2 iff O1 c= O2 & O1 <> O2;
per cases by A5,A6,ORDINAL1:11;
suppose
A8: O2 = O4;
thus (f, O1)+.a [= (f, O2)+.a
proof
per cases by A4,A7,ORDINAL1:11;
suppose
O1 = O2;
hence thesis;
end;
suppose
A9: O1 in O2;
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being Sequence such that
A10: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A11: L1.O1 = (f, O1)+.a & L1.O1 in rng L1 by A9,A10,FUNCT_1:def 3;
(f, O2)+.a = "\/"(rng L1, L) by A2,A8,A10,Th17;
hence thesis by A11,LATTICE3:38;
end;
end;
end;
suppose
O2 in O4;
hence thesis by A3,A4;
end;
end;
end;
assume
A12: a [= f.a;
A13: now
let O4;
assume
A14: S[O4];
thus S[succ O4]
proof
let O1, O2;
assume that
A15: O1 c= O2 and
A16: O2 c= succ O4;
per cases;
suppose
O1 = O2 & O2 <> succ O4;
hence thesis;
end;
suppose
O1 <> O2 & O2 <> succ O4;
then O2 c< succ O4 by A16;
then O2 in succ O4 by ORDINAL1:11;
then O2 c= O4 by ORDINAL1:22;
hence thesis by A14,A15;
end;
suppose
O1 = O2 & O2 = succ O4;
hence thesis;
end;
suppose
A17: O1 <> O2 & O2 = succ O4;
A18: (f, O4)+.a [= (f, succ O4)+.a
proof
per cases by ORDINAL1:29;
suppose
A19: O4 is limit_ordinal;
thus thesis
proof
per cases;
suppose
O4 = {};
then (f, O4)+.a = a by Th13;
hence thesis by A12,Th15;
end;
suppose
A20: O4 <> {};
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being Sequence such that
A21: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
from ORDINAL2:sch 2;
A22: rng L1 is_less_than (f, succ O4)+.a
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A23: O3 in dom L1 and
A24: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A23;
O3 in succ O3 by ORDINAL1:6;
then
A25: O3 c= succ O3 by ORDINAL1:def 2;
O3 c= O4 by A21,A23,ORDINAL1:def 2;
then (f, O3)+.a [= (f, O4)+.a by A14;
then f.(f, O3)+.a [= f.(f, O4)+.a by QUANTAL1:def 12;
then (f, succ O3)+.a [= f.(f, O4)+.a by Th15;
then
A26: (f, succ O3)+.a [= (f, succ O4)+.a by Th15;
succ O3 c= O4 by A21,A23,ORDINAL1:21;
then
A27: (f, O3)+.a [= (f, succ O3)+.a by A14,A25;
q = (f, O3)+.a by A21,A23,A24;
hence q [= (f, succ O4)+.a by A26,A27,LATTICES:7;
end;
(f, O4)+.a = "\/"(rng L1, L) by A19,A20,A21,Th17;
hence thesis by A22,LATTICE3:def 21;
end;
end;
end;
suppose
ex O3 st O4 = succ O3;
then consider O3 such that
A28: O4 = succ O3;
O3 c= O4 by A28,XBOOLE_1:7;
then (f, O3)+.a [= (f, O4)+.a by A14;
then f.((f, O3)+.a) [= f.((f, O4)+.a) by QUANTAL1:def 12;
then (f, O4)+.a [= f.((f, O4)+.a) by A28,Th15;
hence thesis by Th15;
end;
end;
O1 c< O2 by A15,A17;
then O1 in O2 by ORDINAL1:11;
then O1 c= O4 by A17,ORDINAL1:22;
then (f, O1)+.a [= (f, O4)+.a by A14;
hence thesis by A17,A18,LATTICES:7;
end;
end;
end;
let O1, O2;
assume
A29: O1 c= O2;
A30: S[0];
for O4 holds S[O4] from ORDINAL2:sch 1(A30, A13, A1);
hence thesis by A29;
end;
theorem Th25:
for a st f.a [= a for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a
proof
let a;
defpred S[Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O2)-.a
[= (f, O1)-.a;
A1: now
let O4;
assume that
A2: O4 <> 0 & O4 is limit_ordinal and
A3: for O3 st O3 in O4 holds S[O3];
thus S[O4]
proof
let O1, O2;
assume that
A4: O1 c= O2 and
A5: O2 c= O4;
A6: O2 c< O4 iff O2 c= O4 & O2 <> O4;
A7: O1 c< O2 iff O1 c= O2 & O1 <> O2;
per cases by A5,A6,ORDINAL1:11;
suppose
A8: O2 = O4;
thus (f, O2)-.a [= (f, O1)-.a
proof
per cases by A4,A7,ORDINAL1:11;
suppose
O1 = O2;
hence thesis;
end;
suppose
A9: O1 in O2;
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being Sequence such that
A10: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A11: L1.O1 = (f, O1)-.a & L1.O1 in rng L1 by A9,A10,FUNCT_1:def 3;
(f, O2)-.a = "/\"(rng L1, L) by A2,A8,A10,Th18;
hence thesis by A11,LATTICE3:38;
end;
end;
end;
suppose
O2 in O4;
hence thesis by A3,A4;
end;
end;
end;
assume
A12: f.a [= a;
A13: now
let O4;
assume
A14: S[O4];
thus S[succ O4]
proof
let O1, O2;
assume that
A15: O1 c= O2 and
A16: O2 c= succ O4;
per cases;
suppose
O1 = O2 & O2 <> succ O4;
hence thesis;
end;
suppose
O1 <> O2 & O2 <> succ O4;
then O2 c< succ O4 by A16;
then O2 in succ O4 by ORDINAL1:11;
then O2 c= O4 by ORDINAL1:22;
hence thesis by A14,A15;
end;
suppose
O1 = O2 & O2 = succ O4;
hence thesis;
end;
suppose
A17: O1 <> O2 & O2 = succ O4;
A18: (f, succ O4)-.a [= (f, O4)-.a
proof
per cases by ORDINAL1:29;
suppose
A19: O4 is limit_ordinal;
thus thesis
proof
per cases;
suppose
O4 = {};
then (f, O4)-.a = a by Th14;
hence thesis by A12,Th16;
end;
suppose
A20: O4 <> {};
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being Sequence such that
A21: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
from ORDINAL2:sch 2;
A22: (f, succ O4)-.a is_less_than rng L1
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A23: O3 in dom L1 and
A24: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A23;
O3 in succ O3 by ORDINAL1:6;
then
A25: O3 c= succ O3 by ORDINAL1:def 2;
O3 c= O4 by A21,A23,ORDINAL1:def 2;
then (f, O4)-.a [= (f, O3)-.a by A14;
then f.(f, O4)-.a [= f.(f, O3)-.a by QUANTAL1:def 12;
then (f, succ O4)-.a [= f.(f, O3)-.a by Th16;
then
A26: (f, succ O4)-.a [= (f, succ O3)-.a by Th16;
succ O3 c= O4 by A21,A23,ORDINAL1:21;
then
A27: (f, succ O3)-.a [= (f, O3)-.a by A14,A25;
q = (f, O3)-.a by A21,A23,A24;
hence (f, succ O4)-.a [= q by A26,A27,LATTICES:7;
end;
(f, O4)-.a = "/\"(rng L1, L) by A19,A20,A21,Th18;
hence thesis by A22,LATTICE3:34;
end;
end;
end;
suppose
ex O3 st O4 = succ O3;
then consider O3 such that
A28: O4 = succ O3;
O3 c= O4 by A28,XBOOLE_1:7;
then (f, O4)-.a [= (f, O3)-.a by A14;
then f.((f, O4)-.a) [= f.((f, O3)-.a) by QUANTAL1:def 12;
then f.((f, O4)-.a) [= (f, O4)-.a by A28,Th16;
hence thesis by Th16;
end;
end;
O1 c< O2 by A15,A17;
then O1 in O2 by ORDINAL1:11;
then O1 c= O4 by A17,ORDINAL1:22;
then (f, O4)-.a [= (f, O1)-.a by A14;
hence thesis by A17,A18,LATTICES:7;
end;
end;
end;
let O1, O2;
assume
A29: O1 c= O2;
A30: S[0];
for O4 holds S[O4] from ORDINAL2:sch 1(A30, A13, A1);
hence thesis by A29;
end;
theorem Th26:
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
proof
let a;
assume
A1: a [= f.a;
let O1, O2;
A2: (f, O1)+.a [= (f, succ O1)+.a by A1,Th24,XBOOLE_1:7;
assume that
A3: O1 c< O2 and
A4: not (f, O2)+.a is_a_fixpoint_of f and
A5: (f, O1)+.a = (f, O2)+.a;
O1 in O2 by A3,ORDINAL1:11;
then succ O1 c= O2 by ORDINAL1:21;
then (f, succ O1)+.a [= (f, O2)+.a by A1,Th24;
then (f, O1)+.a = (f, succ O1)+.a by A5,A2,LATTICES:8;
then (f, O1)+.a = f.(f, O1)+.a by Th15;
hence contradiction by A4,A5;
end;
theorem Th27:
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
proof
let a;
assume
A1: f.a [= a;
let O1, O2;
A2: (f, succ O1)-.a [= (f, O1)-.a by A1,Th25,XBOOLE_1:7;
assume that
A3: O1 c< O2 and
A4: not (f, O2)-.a is_a_fixpoint_of f and
A5: (f, O1)-.a = (f, O2)-.a;
O1 in O2 by A3,ORDINAL1:11;
then succ O1 c= O2 by ORDINAL1:21;
then (f, O2)-.a [= (f, succ O1)-.a by A1,Th25;
then (f, O1)-.a = (f, succ O1)-.a by A5,A2,LATTICES:8;
then (f, O1)-.a = f.(f, O1)-.a by Th16;
hence contradiction by A4,A5;
end;
theorem Th28:
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
proof
assume that
A1: a [= f.a and
A2: (f, O1)+.a is_a_fixpoint_of f;
set fa = (f, O1)+.a;
defpred S[Ordinal] means O1 c= $1 implies fa = (f, $1)+.a;
A3: now
let O2;
assume that
A4: O2 <> 0 & O2 is limit_ordinal and
A5: for O3 st O3 in O2 holds S[O3];
thus S[O2]
proof
assume O1 c= O2;
then
A6: fa [= (f, O2)+.a by A1,Th24;
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being Sequence such that
A7: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A8: rng L1 is_less_than fa
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A9: O3 in dom L1 and
A10: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A9;
per cases;
suppose
O1 c= O3;
then (f, O3)+.a [= fa by A5,A7,A9;
hence q [= fa by A7,A9,A10;
end;
suppose
O3 c= O1;
then (f, O3)+.a [= fa by A1,Th24;
hence q [= fa by A7,A9,A10;
end;
end;
(f, O2)+.a = "\/"(rng L1, L) by A4,A7,Th17;
then (f, O2)+.a [= fa by A8,LATTICE3:def 21;
hence thesis by A6,LATTICES:8;
end;
end;
A11: now
let O2;
assume
A12: S[O2];
thus S[succ O2]
proof
assume
A13: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
O1 <> succ O2;
then O1 c< succ O2 by A13;
then O1 in succ O2 by ORDINAL1:11;
hence fa = f.(f, O2)+.a by A2,A12,ORDINAL1:22
.= (f, succ O2)+.a by Th15;
end;
end;
end;
A14: S[0];
thus for O2 holds S[O2] from ORDINAL2:sch 1(A14, A11, A3);
end;
theorem Th29:
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
proof
assume that
A1: f.a [= a and
A2: (f, O1)-.a is_a_fixpoint_of f;
set fa = (f, O1)-.a;
defpred S[Ordinal] means O1 c= $1 implies fa = (f, $1)-.a;
A3: now
let O2;
assume that
A4: O2 <> 0 & O2 is limit_ordinal and
A5: for O3 st O3 in O2 holds S[O3];
thus S[O2]
proof
assume O1 c= O2;
then
A6: (f, O2)-.a [= fa by A1,Th25;
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being Sequence such that
A7: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A8: fa is_less_than rng L1
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A9: O3 in dom L1 and
A10: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A9;
per cases;
suppose
O1 c= O3;
then fa [= (f, O3)-.a by A5,A7,A9;
hence fa [= q by A7,A9,A10;
end;
suppose
O3 c= O1;
then fa [= (f, O3)-.a by A1,Th25;
hence fa [= q by A7,A9,A10;
end;
end;
(f, O2)-.a = "/\"(rng L1, L) by A4,A7,Th18;
then fa [= (f, O2)-.a by A8,LATTICE3:39;
hence thesis by A6,LATTICES:8;
end;
end;
A11: now
let O2;
assume
A12: S[O2];
thus S[succ O2]
proof
assume
A13: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
O1 <> succ O2;
then O1 c< succ O2 by A13;
then O1 in succ O2 by ORDINAL1:11;
hence fa = f.(f, O2)-.a by A2,A12,ORDINAL1:22
.= (f, succ O2)-.a by Th16;
end;
end;
end;
A14: S[0];
thus for O2 holds S[O2] from ORDINAL2:sch 1(A14, A11, A3);
end;
Lm1: O1 c< O2 or O1 = O2 or O2 c< O1
proof
assume that
A1: ( not O1 c< O2)& not O1 = O2 and
A2: not O2 c< O1;
not O1 c= O2 by A1;
hence contradiction by A2;
end;
theorem Th30:
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
proof
let a;
set cL = the carrier of L;
set ccL = card cL;
set nccL = nextcard ccL;
deffunc F(Ordinal)=(f, $1)+.a;
consider Ls being Sequence such that
A1: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(
O2) from ORDINAL2:sch 2;
assume
A2: a [= f.a;
now
assume
A3: for O st O in nccL holds not (f, O)+.a is_a_fixpoint_of f;
A4: Ls is one-to-one
proof
let x1,x2 be object;
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls.x1 = Ls.x2;
reconsider x1, x2 as Ordinal by A5,A6;
A8: Ls.x1 = (f, x1)+.a by A1,A5;
A9: Ls.x2 = (f, x2)+.a by A1,A6;
per cases by Lm1;
suppose
A10: x1 c< x2;
not (f, x2)+.a is_a_fixpoint_of f by A1,A3,A6;
hence thesis by A2,A1,A6,A7,A8,A10,Th26;
end;
suppose
A11: x2 c< x1;
not (f, x1)+.a is_a_fixpoint_of f by A1,A3,A5;
hence thesis by A2,A1,A5,A7,A9,A11,Th26;
end;
suppose
x2 = x1;
hence thesis;
end;
end;
rng Ls c= cL
proof
let y be object;
assume y in rng Ls;
then consider x being object such that
A12: x in dom Ls and
A13: Ls.x = y by FUNCT_1:def 3;
reconsider x as Ordinal by A12;
Ls.x = (f, x)+.a by A1,A12;
hence thesis by A13;
end;
then card nccL c= ccL by A1,A4,CARD_1:10;
then
A14: nccL c= ccL;
ccL in nccL by CARD_1:18;
hence contradiction by A14,CARD_1:4;
end;
then consider O such that
A15: O in nccL and
A16: (f, O)+.a is_a_fixpoint_of f;
take O;
card O in nccL by A15,CARD_1:9;
hence card O c= card cL by CARD_3:91;
thus thesis by A16;
end;
theorem Th31:
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
proof
let a;
set cL = the carrier of L;
set ccL = card cL;
set nccL = nextcard ccL;
deffunc F(Ordinal)=(f, $1)-.a;
consider Ls being Sequence such that
A1: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(
O2) from ORDINAL2:sch 2;
assume
A2: f.a [= a;
now
assume
A3: for O st O in nccL holds not (f, O)-.a is_a_fixpoint_of f;
A4: Ls is one-to-one
proof
let x1,x2 be object;
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls.x1 = Ls.x2;
reconsider x1, x2 as Ordinal by A5,A6;
A8: Ls.x1 = (f, x1)-.a by A1,A5;
A9: Ls.x2 = (f, x2)-.a by A1,A6;
per cases by Lm1;
suppose
A10: x1 c< x2;
not (f, x2)-.a is_a_fixpoint_of f by A1,A3,A6;
hence thesis by A2,A1,A6,A7,A8,A10,Th27;
end;
suppose
A11: x2 c< x1;
not (f, x1)-.a is_a_fixpoint_of f by A1,A3,A5;
hence thesis by A2,A1,A5,A7,A9,A11,Th27;
end;
suppose
x2 = x1;
hence thesis;
end;
end;
rng Ls c= cL
proof
let y be object;
assume y in rng Ls;
then consider x being object such that
A12: x in dom Ls and
A13: Ls.x = y by FUNCT_1:def 3;
reconsider x as Ordinal by A12;
Ls.x = (f, x)-.a by A1,A12;
hence thesis by A13;
end;
then card nccL c= ccL by A1,A4,CARD_1:10;
then
A14: nccL c= ccL;
ccL in nccL by CARD_1:18;
hence contradiction by A14,CARD_1:4;
end;
then consider O such that
A15: O in nccL and
A16: (f, O)-.a is_a_fixpoint_of f;
take O;
card O in nccL by A15,CARD_1:9;
hence card O c= card cL by CARD_3:91;
thus thesis by A16;
end;
theorem Th32:
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)
proof
let a, b;
reconsider ab = a"\/"b as Element of L;
A1: a [= ab by LATTICES:5;
then
A2: f.a [= f.ab by QUANTAL1:def 12;
A3: b [= ab by LATTICES:5;
then
A4: f.b [= f.ab by QUANTAL1:def 12;
assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then
A5: a = f.a & b = f.b;
then consider O such that
A6: card O c= card the carrier of L & (f, O)+.ab is_a_fixpoint_of f by A2,A4
,Th30,FILTER_0:6;
take O;
thus card O c= card the carrier of L & (f, O)+.(a"\/"b) is_a_fixpoint_of f
by A6;
ab [= f.ab by A5,A2,A4,FILTER_0:6;
then
A7: ab [= (f, O)+.(a"\/"b) by Th22;
hence a [= (f, O)+.(a"\/"b) by A1,LATTICES:7;
thus thesis by A3,A7,LATTICES:7;
end;
theorem Th33:
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
proof
let a, b;
reconsider ab = a"/\"b as Element of L;
A1: ab [= a by LATTICES:6;
then
A2: f.ab [= f.a by QUANTAL1:def 12;
A3: ab [= b by LATTICES:6;
then
A4: f.ab [= f.b by QUANTAL1:def 12;
assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then
A5: a = f.a & b = f.b;
then consider O such that
A6: card O c= card the carrier of L & (f, O)-.ab is_a_fixpoint_of f by A2,A4
,Th31,FILTER_0:7;
take O;
thus card O c= card the carrier of L & (f, O)-.(a"/\"b) is_a_fixpoint_of f
by A6;
f.ab [= ab by A5,A2,A4,FILTER_0:7;
then
A7: (f, O)-.(a"/\"b) [= ab by Th23;
hence (f, O)-.(a"/\"b) [= a by A1,LATTICES:7;
thus thesis by A3,A7,LATTICES:7;
end;
theorem Th34:
a [= b & b is_a_fixpoint_of f implies for O2 holds (f, O2)+.a [= b
proof
assume that
A1: a [= b and
A2: b is_a_fixpoint_of f;
defpred S[Ordinal] means (f, $1)+.a [= b;
A3: f.b = b by A2;
A4: now
let O1;
assume S[O1];
then f.(f, O1)+.a [= f.b by QUANTAL1:def 12;
hence S[succ O1] by A3,Th15;
end;
A5: now
deffunc F(Ordinal)=(f, $1)+.a;
let O1;
assume that
A6: O1 <> 0 & O1 is limit_ordinal and
A7: for O2 st O2 in O1 holds S[O2];
consider L1 being Sequence such that
A8: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A9: rng L1 is_less_than b
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A10: O3 in dom L1 and
A11: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A10;
(f, O3)+.a [= b by A7,A8,A10;
hence q [= b by A8,A10,A11;
end;
(f, O1)+.a = "\/"(rng L1, L) by A6,A8,Th17;
hence S[O1] by A9,LATTICE3:def 21;
end;
A12: S[0] by A1,Th13;
thus for O2 holds S[O2] from ORDINAL2:sch 1(A12, A4, A5);
end;
theorem Th35:
b [= a & b is_a_fixpoint_of f implies for O2 holds b [= (f, O2) -.a
proof
assume that
A1: b [= a and
A2: b is_a_fixpoint_of f;
defpred S[Ordinal] means b [= (f, $1)-.a;
A3: f.b = b by A2;
A4: now
let O1;
assume S[O1];
then f.b [= f.(f, O1)-.a by QUANTAL1:def 12;
hence S[succ O1] by A3,Th16;
end;
A5: now
deffunc F(Ordinal)=(f, $1)-.a;
let O1;
assume that
A6: O1 <> 0 & O1 is limit_ordinal and
A7: for O2 st O2 in O1 holds S[O2];
consider L1 being Sequence such that
A8: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A9: b is_less_than rng L1
proof
let q be Element of L;
assume q in rng L1;
then consider O3 being object such that
A10: O3 in dom L1 and
A11: q = L1.O3 by FUNCT_1:def 3;
reconsider O3 as Ordinal by A10;
b [= (f, O3)-.a by A7,A8,A10;
hence b [= q by A8,A10,A11;
end;
(f, O1)-.a = "/\"(rng L1, L) by A6,A8,Th18;
hence S[O1] by A9,LATTICE3:39;
end;
A12: S[0] by A1,Th14;
thus for O2 holds S[O2] from ORDINAL2:sch 1(A12, A4, A5);
end;
definition
let L be complete Lattice, f be UnOp of L such that
A1: f is monotone;
func FixPoints f -> strict Lattice means
:Def9:
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
defpred P[set] means $1 is_a_fixpoint_of f;
set P = {x where x is Element of L: P[x]};
A2: P is Subset of L from DOMAIN_1:sch 7;
consider a being Element of L such that
A3: a is_a_fixpoint_of f by A1,Th21;
A4: a in P by A3;
reconsider P as Subset of L by A2;
A5: P is with_suprema
proof
let x,y be Element of L;
assume that
A6: x in P and
A7: y in P;
consider a being Element of L such that
A8: x = a and
A9: a is_a_fixpoint_of f by A6;
consider b being Element of L such that
A10: y = b and
A11: b is_a_fixpoint_of f by A7;
reconsider a, b as Element of L;
reconsider ab = a"\/"b as Element of L;
consider O such that
card O c= card the carrier of L and
A12: (f, O)+.ab is_a_fixpoint_of f and
A13: a [= (f, O)+.ab & b [= (f, O)+.ab by A1,A9,A11,Th32;
set z = (f, O)+.ab;
take z;
thus z in P by A12;
thus x [= z & y [= z by A8,A10,A13;
let z9 be Element of L;
assume that
A14: z9 in P and
A15: x [= z9 & y [= z9;
A16: ex zz being Element of L st zz = z9 & zz is_a_fixpoint_of f by A14;
ab [= z9 by A8,A10,A15,FILTER_0:6;
hence z [= z9 by A1,A16,Th34;
end;
P is with_infima
proof
let x,y be Element of L;
assume that
A17: x in P and
A18: y in P;
consider a being Element of L such that
A19: x = a and
A20: a is_a_fixpoint_of f by A17;
consider b being Element of L such that
A21: y = b and
A22: b is_a_fixpoint_of f by A18;
reconsider a, b as Element of L;
reconsider ab = a"/\"b as Element of L;
consider O such that
card O c= card the carrier of L and
A23: (f, O)-.ab is_a_fixpoint_of f and
A24: (f, O)-.ab [= a & (f, O)-.ab [= b by A1,A20,A22,Th33;
set z = (f, O)-.ab;
take z;
thus z in P by A23;
thus z [= x & z [= y by A19,A21,A24;
let z9 be Element of L;
assume that
A25: z9 in P and
A26: z9 [= x & z9 [= y;
A27: ex zz being Element of L st zz = z9 & zz is_a_fixpoint_of f by A25;
z9 [= ab by A19,A21,A26,FILTER_0:7;
hence z9 [= z by A1,A27,Th35;
end;
then reconsider
P as non empty with_suprema with_infima Subset of L by A4,A5;
take latt P, P;
thus P = {x where x is Element of L: x is_a_fixpoint_of f};
thus thesis;
end;
uniqueness;
end;
theorem Th36:
the carrier of FixPoints f = {x where x is Element of L: x
is_a_fixpoint_of f}
proof
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} & FixPoints f = latt P by Def9;
hence thesis by Def8;
end;
theorem Th37:
the carrier of FixPoints f c= the carrier of L
proof
A1: the carrier of FixPoints f = {x where x is Element of L: x
is_a_fixpoint_of f} by Th36;
let x be object;
assume x in the carrier of FixPoints f;
then ex a st x = a & a is_a_fixpoint_of f by A1;
hence thesis;
end;
theorem Th38:
a in the carrier of FixPoints f iff a is_a_fixpoint_of f
proof
A1: the carrier of FixPoints f = {x where x is Element of L: x
is_a_fixpoint_of f} by Th36;
hereby
assume a in the carrier of FixPoints f;
then ex b st a = b & b is_a_fixpoint_of f by A1;
hence a is_a_fixpoint_of f;
end;
assume a is_a_fixpoint_of f;
hence thesis by A1;
end;
theorem Th39:
for x, y being Element of FixPoints f, a, b st x = a & y = b
holds (x [= y iff a [= b)
proof
A1: 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} & FixPoints f = latt P by Def9;
let x, y be Element of FixPoints f, a, b;
assume
A2: x = a & y = b;
ex a9, b9 being Element of L st x = a9 & y = b9 &( x [= y iff a9 [= b9)
by A1,Def8;
hence thesis by A2;
end;
theorem
FixPoints f is complete
proof
set F = FixPoints f;
set cF = the carrier of F;
set cL = the carrier of L;
let X be set;
set Y = X /\ cF;
set s = "\/"(Y, L);
A1: Y c= cF by XBOOLE_1:17;
Y is_less_than f.s
proof
let q be Element of cL;
reconsider q9 = q as Element of L;
assume
A2: q in Y;
then q [= s by LATTICE3:38;
then
A3: f.q [= f.s by QUANTAL1:def 12;
q9 is_a_fixpoint_of f by A1,A2,Th38;
hence q [= f.s by A3;
end;
then
A4: s [= f.s by LATTICE3:def 21;
then consider O such that
card O c= card cL and
A5: (f, O)+.s is_a_fixpoint_of f by Th30;
reconsider p9 = (f, O)+.s as Element of L;
reconsider p = p9 as Element of cF by A5,Th38;
take p;
thus X is_less_than p
proof
let q be Element of cF;
q in cF & cF c= cL by Th37;
then reconsider qL9 = q as Element of L;
assume q in X;
then q in Y by XBOOLE_0:def 4;
then
A6: qL9 [= s by LATTICE3:38;
s [= p9 by A4,Th22;
then qL9 [= p9 by A6,LATTICES:7;
hence q [= p by Th39;
end;
let r be Element of cF such that
A7: X is_less_than r;
reconsider r99 = r as Element of F;
cF = {x where x is Element of L: x is_a_fixpoint_of f} & r in the
carrier of F by Th36;
then consider r9 being Element of L such that
A8: r9 = r and
A9: r9 is_a_fixpoint_of f;
A10: Y c= X by XBOOLE_1:17;
Y is_less_than r9
proof
let q be Element of cL;
assume
A11: q in Y;
then reconsider q99 = q as Element of F by A1;
q99 [= r99 by A10,A7,A11;
hence q [= r9 by A8,Th39;
end;
then s [= r9 by LATTICE3:def 21;
then p9 [= r9 by A9,Th34;
hence p [= r by A8,Th39;
end;
definition
let L, f;
func lfp f -> Element of L equals
(f, nextcard the carrier of L)+.Bottom L;
coherence;
func gfp f -> Element of L equals
(f, nextcard the carrier of L)-.Top L;
coherence;
end;
theorem Th41:
lfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
L & (f, O)+.Bottom L = lfp f
proof
reconsider ze = Bottom L as Element of L;
A1: Bottom L [= f.ze by LATTICES:16;
then consider O such that
A2: card O c= card the carrier of L and
A3: (f, O)+.Bottom L is_a_fixpoint_of f by Th30;
card the carrier of L in nextcard the carrier of L by CARD_1:def 3;
then card O in nextcard the carrier of L by A2,ORDINAL1:12;
then O in nextcard the carrier of L by CARD_3:44;
then
A4: O c= nextcard the carrier of L by ORDINAL1:def 2;
hence lfp f is_a_fixpoint_of f by A1,A3,Th28;
take O;
thus card O c= card the carrier of L by A2;
thus thesis by A1,A3,A4,Th28;
end;
theorem Th42:
gfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
L & (f, O)-.Top L = gfp f
proof
reconsider je = Top L as Element of L;
A1: f.je [= Top L by LATTICES:19;
then consider O such that
A2: card O c= card the carrier of L and
A3: (f, O)-.Top L is_a_fixpoint_of f by Th31;
card the carrier of L in nextcard the carrier of L by CARD_1:def 3;
then card O in nextcard the carrier of L by A2,ORDINAL1:12;
then O in nextcard the carrier of L by CARD_3:44;
then
A4: O c= nextcard the carrier of L by ORDINAL1:def 2;
hence gfp f is_a_fixpoint_of f by A1,A3,Th29;
take O;
thus card O c= card the carrier of L by A2;
thus thesis by A1,A3,A4,Th29;
end;
theorem Th43:
a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f
proof
defpred S[Ordinal] means (f, $1)+.Bottom L [= a;
A1: now
deffunc F(Ordinal)=(f, $1)+.Bottom L;
let O1;
assume that
A2: O1 <> 0 & O1 is limit_ordinal and
A3: for O2 st O2 in O1 holds S[O2];
consider L1 being Sequence such that
A4: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A5: rng L1 is_less_than a
proof
let q be Element of L;
assume q in rng L1;
then consider C being object such that
A6: C in dom L1 and
A7: q = L1.C by FUNCT_1:def 3;
reconsider C as Ordinal by A6;
(f, C)+.Bottom L [= a by A3,A4,A6;
hence q [= a by A4,A6,A7;
end;
(f, O1)+.Bottom L = "\/"(rng L1, L) by A2,A4,Th17;
hence S[O1] by A5,LATTICE3:def 21;
end;
assume a is_a_fixpoint_of f;
then
A8: f.a = a;
A9: now
let O1;
assume S[O1];
then f.(f, O1)+.Bottom L [= f.a by QUANTAL1:def 12;
hence S[succ O1] by A8,Th15;
end;
(f, {})+.Bottom L = Bottom L by Th13;
then
A10: S[0] by LATTICES:16;
for O2 holds S[O2] from ORDINAL2:sch 1(A10, A9, A1);
hence lfp f [= a;
defpred S[Ordinal] means a [= (f, $1)-.Top L;
A11: now
let O1;
assume S[O1];
then f.a [= f.(f, O1)-.Top L by QUANTAL1:def 12;
hence S[succ O1] by A8,Th16;
end;
A12: now
deffunc F(Ordinal)=(f, $1)-.Top L;
let O1;
assume that
A13: O1 <> 0 & O1 is limit_ordinal and
A14: for O2 st O2 in O1 holds S[O2];
consider L1 being Sequence such that
A15: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
ORDINAL2:sch 2;
A16: a is_less_than rng L1
proof
let q be Element of L;
assume q in rng L1;
then consider C being object such that
A17: C in dom L1 and
A18: q = L1.C by FUNCT_1:def 3;
reconsider C as Ordinal by A17;
a [= (f, C)-.Top L by A14,A15,A17;
hence a [= q by A15,A17,A18;
end;
(f, O1)-.Top L = "/\"(rng L1, L) by A13,A15,Th18;
hence S[O1] by A16,LATTICE3:39;
end;
(f, {})-.Top L = Top L by Th14;
then
A19: S[0] by LATTICES:19;
for O2 holds S[O2] from ORDINAL2:sch 1(A19, A11, A12);
hence thesis;
end;
theorem
f.a [= a implies lfp f [= a
proof
assume
A1: f.a [= a;
then consider O such that
card O c= card the carrier of L and
A2: (f, O)-.a is_a_fixpoint_of f by Th31;
A3: lfp f [= (f, O)-.a by A2,Th43;
(f, O)-.a [= a by A1,Th23;
hence thesis by A3,LATTICES:7;
end;
theorem
a [= f.a implies a [= gfp f
proof
assume
A1: a [= f.a;
then consider O such that
card O c= card the carrier of L and
A2: (f, O)+.a is_a_fixpoint_of f by Th30;
A3: (f, O)+.a [= gfp f by A2,Th43;
a [= (f, O)+.a by A1,Th22;
hence thesis by A3,LATTICES:7;
end;
begin :: Boolean Lattices
reserve f for monotone UnOp of BooleLatt A;
theorem Th46:
for f being UnOp of BooleLatt A holds f is monotone iff f is c=-monotone
proof
let f be UnOp of BooleLatt A;
thus f is monotone implies f is c=-monotone
proof
assume
A1: f is monotone;
let x, y be Element of BooleLatt A;
assume x c= y;
then x [= y by LATTICE3:2;
then f.x [= f.y by A1;
hence thesis by LATTICE3:2;
end;
assume
A2: f is c=-monotone;
let p, q be Element of BooleLatt A;
assume p [= q;
then p c= q by LATTICE3:2;
then f.p c= f.q by A2;
hence f.p [= f.q by LATTICE3:2;
end;
theorem
ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f
proof
reconsider lf = lfp f as Subset of A by LATTICE3:def 1;
the carrier of BooleLatt A = bool A by LATTICE3:def 1;
then reconsider g = f as c=-monotone Function of bool A, bool A by Th46;
reconsider lg = lfp(A, g) as Element of BooleLatt A by LATTICE3:def 1;
take g;
lg is_a_fixpoint_of f by Th4;
then lfp f [= lg by Th43;
then
A1: lf c= lg by LATTICE3:2;
lfp f is_a_fixpoint_of f by Th41;
then lfp (A, g) c= lf by Th8;
hence thesis by A1;
end;
theorem
ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f
proof
reconsider gf = gfp f as Subset of A by LATTICE3:def 1;
the carrier of BooleLatt A = bool A by LATTICE3:def 1;
then reconsider g = f as c=-monotone Function of bool A, bool A by Th46;
reconsider gg = gfp(A, g) as Element of BooleLatt A by LATTICE3:def 1;
take g;
gg is_a_fixpoint_of f by Th5;
then gg [= gfp f by Th43;
then
A1: gg c= gf by LATTICE3:2;
gfp f is_a_fixpoint_of f by Th42;
then gf c= gfp (A, g) by Th8;
hence thesis by A1;
end;