Copyright (c) 1996 Association of Mizar Users
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;
definitions TARSKI, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0;
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_1, RELAT_2, ORDINAL1,
CARD_3, CARD_4, PROB_1, XBOOLE_0, XBOOLE_1, FUNCT_7, PARTFUN1;
schemes NAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, ORDINAL2;
begin :: Preliminaries
reserve f, g, h for Function;
theorem Th1:
f is one-to-one & g is one-to-one & rng f misses rng g
implies f+*g is one-to-one
proof assume
A1: f is one-to-one & g is one-to-one & rng f misses rng g;
set fg = f+*g;
let x1,x2 be set; assume
A2: x1 in dom fg & x2 in dom fg & fg.x1 = fg.x2;
then A3: (x1 in dom f or x1 in dom g) & (x2 in dom f or x2 in dom g)
by FUNCT_4:13;
per cases;
suppose A4: x1 in dom g & x2 in dom g;
then fg.x1 = g.x1 & fg.x2 = g.x2 by FUNCT_4:14;
hence x1 = x2 by A1,A2,A4,FUNCT_1:def 8;
suppose A5: x1 in dom g & not x2 in dom g;
then A6: x2 in dom f by A2,FUNCT_4:13;
A7: fg.x1 = g.x1 & fg.x2 = f.x2 by A5,FUNCT_4:12,14;
g.x1 in rng g & f.x2 in rng f by A5,A6,FUNCT_1:def 5;
hence x1 = x2 by A1,A2,A7,XBOOLE_0:3;
suppose A8: not x1 in dom g & x2 in dom g;
then A9: x1 in dom f by A2,FUNCT_4:13;
A10: fg.x1 = f.x1 & fg.x2 = g.x2 by A8,FUNCT_4:12,14;
g.x2 in rng g & f.x1 in rng f by A8,A9,FUNCT_1:def 5;
hence x1 = x2 by A1,A2,A10,XBOOLE_0:3;
suppose A11: not x1 in dom g & not x2 in dom g;
then fg.x1 = f.x1 & fg.x2 = f.x2 by FUNCT_4:12;
hence x1 = x2 by A1,A2,A3,A11,FUNCT_1:def 8;
end;
canceled;
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
A1: h = f \/ g & dom f misses dom g;
then A2: dom h = dom f \/ dom g by RELAT_1:13;
hereby assume
A3: h is one-to-one;
thus f is one-to-one proof assume not f is one-to-one;
then consider x1, x2 being set such that
A4: x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1<>x2 by FUNCT_1:def 8;
[x1, f.x1] in f & [x2, f.x2] in f by A4,FUNCT_1:def 4;
then A5: [x1, f.x1] in h & [x2, f.x2] in h by A1,XBOOLE_0:def 2;
A6: x1 in dom h & x2 in dom h by A2,A4,XBOOLE_0:def 2;
then f.x1 = h.x1 & f.x2 = h.x2 by A5,FUNCT_1:def 4;
hence contradiction by A3,A4,A6,FUNCT_1:def 8;
end;
thus g is one-to-one proof assume not g is one-to-one;
then consider x1, x2 being set such that
A7: x1 in dom g & x2 in dom g & g.x1 = g.x2 & x1<>x2 by FUNCT_1:def 8;
[x1, g.x1] in g & [x2, g.x2] in g by A7,FUNCT_1:def 4;
then A8: [x1, g.x1] in h & [x2, g.x2] in h by A1,XBOOLE_0:def 2;
A9: x1 in dom h & x2 in dom h by A2,A7,XBOOLE_0:def 2;
then g.x1 = h.x1 & g.x2 = h.x2 by A8,FUNCT_1:def 4;
hence contradiction by A3,A7,A9,FUNCT_1:def 8;
end;
thus rng f misses rng g proof assume not thesis;
then consider hx being set such that
A10: hx in rng f & hx in rng g by XBOOLE_0:3;
consider x1 being set such that
A11: x1 in dom f & hx = f.x1 by A10,FUNCT_1:def 5;
consider x2 being set such that
A12: x2 in dom g & hx = g.x2 by A10,FUNCT_1:def 5;
A13: x1 <> x2 by A1,A11,A12,XBOOLE_0:3;
[x1, hx] in f & [x2, hx] in g by A11,A12,FUNCT_1:def 4;
then A14: [x1, hx] in h & [x2, hx] in h by A1,XBOOLE_0:def 2;
A15: x1 in dom h & x2 in dom h by A2,A11,A12,XBOOLE_0:def 2;
then h.x1 = hx & h.x2 = hx by A14,FUNCT_1:def 4;
hence contradiction by A3,A13,A15,FUNCT_1:def 8;
end;
end;
assume
A16: f is one-to-one & g is one-to-one & rng f misses rng g;
f \/ g = f+*g by A1,FUNCT_4:32;
hence h is one-to-one by A1,A16,Th1;
end;
begin :: Fix points in general
definition
let x be set, f be Function;
pred x is_a_fixpoint_of f means
:Def1: 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
:Def2: a = f.a;
compatibility proof
thus a is_a_fixpoint_of f implies a = f.a by Def1;
assume
A1: a = f.a;
a in A;
hence a in dom f by FUNCT_2:67;
thus a = f.a by A1;
end;
end;
reserve x, y, z, u, X for set,
A for non empty set,
n for Nat,
f for Function of X, X;
theorem Th4:
x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f,n)
proof
assume x is_a_fixpoint_of iter(f,n);
then A1: x in dom iter(f, n) & x = iter(f, n).x by Def1;
iter(f, n) is Function of X, X by FUNCT_7:85;
then A2: dom f = X & rng f c= X & dom iter(f, n) = X by FUNCT_2:67;
then f.x in rng f by A1,FUNCT_1:def 5;
hence f.x in dom iter(f, n) by A2;
thus f.x = (f*iter(f, n)).x by A1,FUNCT_1:23
.= iter(f, n+1).x by FUNCT_7:73
.= (iter(f, n)*f).x by FUNCT_7:71
.= iter(f, n).(f.x) by A1,A2,FUNCT_1:23;
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;
iter(f, n) is Function of X, X by FUNCT_7:85;
then dom f = X & dom iter(f, n) = X by FUNCT_2:67;
hence x in dom f by A1,Def1;
f.x is_a_fixpoint_of iter(f, n) by A1,Th4;
hence x = f.x by A2;
end;
definition let A, B be non empty set, f be Function of A, B;
redefine attr f is c=-monotone means
:Def3: 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
by COHSP_1:def 12;
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;
definition let A be set, B be non empty set;
cluster c=-monotone Function of A, B;
existence proof
consider b being Element of B;
reconsider f = A --> b as Function of A, B by FUNCOP_1:58;
take f;
let x, y be set; assume
A1: x in dom f & y in dom f & x c= y;
then f.x = b by FUNCOP_1:13 .= f.y by A1,FUNCOP_1:13;
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
:Def4: 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 of bool X
from SubsetD;
reconsider H as Subset-Family of X by SETFAM_1:def 7;
meet H is Subset of X;
hence thesis;
end;
func gfp (X, f) -> Subset of X equals
:Def5: 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 of bool X
from SubsetD;
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 Th6:
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 of bool X
from SubsetD;
reconsider H as Subset-Family of X by SETFAM_1:def 7;
set A = meet H;
A1: lfp(X,f) = A by Def4;
now X c= X;
then reconsider X' = X as Element of bool X;
f.X' c= X'; then X' in H;
hence H <> {};
let h be set; assume
A2: h in H; then consider x being Subset of X such that
A3: x = h & f.x c= x;
A c= h by A2,SETFAM_1:4; then f.A c= f.x by A3,Def3;
hence f.A c= h by A3,XBOOLE_1:1;
end;
then A4: f.A c= A by SETFAM_1:6;
then f.(f.A) c= f.A by Def3; then f.A in H; then A c= f.A by SETFAM_1:4;
hence f.(lfp(X,f)) = lfp(X,f) by A1,A4,XBOOLE_0:def 10;
end;
theorem Th7:
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 of bool X from SubsetD;
set A = union H;
A1: gfp(X,f) = A by Def5;
now let x be set; assume
A2: x in H; then consider h being Subset of X such that
A3: x = h & h c= f.h;
h c= A by A2,A3,ZFMISC_1:92; then f.h c= f.A by Def3;
hence x c= f.A by A3,XBOOLE_1:1;
end;
then A4: A c= f.A by ZFMISC_1:94; then f.A c= f.(f.A) by Def3;
then f.A in H; then f.A c= A by ZFMISC_1:92;
hence f.(gfp (X,f)) = gfp(X,f) by A1,A4,XBOOLE_0:def 10;
end;
theorem Th8:
f.S c= S implies lfp(X,f) c= S
proof
set H = {h where h is Subset of X : f.h c= h };
A1: lfp(X,f) = meet H by Def4;
assume f.S c= S; then S in H;
hence lfp(X,f) c= S by A1,SETFAM_1:4;
end;
theorem Th9:
S c= f.S implies S c= gfp(X,f)
proof
set H = {h where h is Subset of X : h c= f.h };
A1: gfp(X,f) = union H by Def5;
assume S c= f.S; then S in H;
hence S c= gfp(X,f) by A1,ZFMISC_1:92;
end;
theorem Th10:
S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f)
proof
assume S = f.S;
hence lfp(X,f) c= S & S c= gfp(X,f) by Th8,Th9;
end;
scheme Knaster{A() -> set, F(set) -> 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
deffunc G(set)=F($1);
consider f being Function such that
A3: dom f = bool A() & for x being set st x in bool A() holds f.x = G(x)
from Lambda;
rng f c= bool A() proof
let x be set; assume x in rng f; then consider y being set such that
A4: y in dom f & x = f.y by FUNCT_1:def 5;
F(y) c= F(A()) by A1,A3,A4;
then F(y) c= A() by A2,XBOOLE_1:1; then f.y c= A() by A3,A4;
hence x in bool A() by A4;
end;
then reconsider f as Function of bool A(), bool A()
by A3,FUNCT_2:def 1,RELSET_1:11;
now let a, b be set; assume
A5: a in dom f & b in dom f & a c= b;
then f.a = F(a) & f.b = F(b) by A3;
hence f.a c= f.b by A1,A5;
end;
then reconsider f as c=-monotone Function of bool A(), bool A() by COHSP_1:def
12;
take d = lfp(A(), f);
d is_a_fixpoint_of f by Th6; then d = f.d by Def1;
hence F(d) = d by A3;
thus d c= A();
end;
reserve X, Y for non empty set,
f for Function of X, Y,
g for Function of Y, X;
theorem Th11: :: 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
proof
deffunc F(set)=X\g.:(Y\f.:$1);
A1: now let x be set; assume x in bool X; X\g.:(Y\f.:x) c= X by XBOOLE_1:36;
hence F(x) in bool X;
end;
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 Lambda1(A1);
now let x, y be set; assume
A3: x in dom h & y in dom h & x c= y;
then f.:x c= f.:y by RELAT_1:156;
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:156;
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,A3;
end;
then reconsider h as c=-monotone Function of bool X, bool X by COHSP_1:def 12
;
take Xa = lfp (X, h); take Xb = X \ Xa; take Ya = f.:Xa; take Yb = Y \ Ya;
thus Xa misses Xb by PROB_1:13; thus Ya misses Yb by PROB_1:13;
thus Xa \/ Xb = X by XBOOLE_1:45; thus Ya \/ Yb = Y by XBOOLE_1:45;
thus f.:Xa = Ya;
A4: Xa is_a_fixpoint_of h by Th6;
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 A4,Def1;
end;
theorem Th12: :: Schroeder-Bernstein
f is one-to-one & g is one-to-one implies
ex h being Function of X,Y st h is bijective
proof assume
A1: f is one-to-one & g is one-to-one;
consider Xa, Xb, Ya, Yb being set such that
A2: Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y &
f.:Xa = Ya & g.:Yb = Xb by Th11;
set fXa = f|Xa; set gYb = g|Yb; set h = fXa+*gYb";
A3: dom f = X by FUNCT_2:def 1; Xa c= X by A2,XBOOLE_1:7;
then A4: dom fXa = Xa by A3,RELAT_1:91;
A5: rng fXa = Ya by A2,RELAT_1:148;
A6: fXa is one-to-one by A1,FUNCT_1:84;
A7: dom g = Y by FUNCT_2:def 1; Yb c= Y by A2,XBOOLE_1:7;
then A8: dom gYb = Yb by A7,RELAT_1:91;
A9: gYb is one-to-one by A1,FUNCT_1:84; rng gYb = Xb by A2,RELAT_1:148;
then A10: dom (gYb") = Xb by A9,FUNCT_1:54;
then A11: X = dom h by A2,A4,FUNCT_4:def 1;
A12: rng (gYb") = Yb by A8,A9,FUNCT_1:55;
fXa \/ gYb" = h by A2,A4,A10,FUNCT_4:32;
then A13: rng h = Y by A2,A5,A12,RELAT_1:26;
then reconsider h as Function of X, Y by A11,FUNCT_2:def 1,RELSET_1:11;
take h;
gYb" is one-to-one by A9,FUNCT_1:62;
then A14: h is one-to-one by A2,A5,A6,A12,Th1;
h is onto by A13,FUNCT_2:def 3;
hence h is bijective by A14,FUNCT_2:def 4;
end;
theorem Th13:
(ex f st f is bijective) implies X,Y are_equipotent
proof given h being Function of X, Y such that
A1: h is bijective;
A2: h is one-to-one onto by A1,FUNCT_2:def 4;
then A3: rng h = Y by FUNCT_2:def 3;
take h;
hereby let x; assume
A4: x in X;
then A5: x in dom h by FUNCT_2:def 1;
take y = h.x;
thus y in Y by A3,A4,FUNCT_2:6;
thus [x,y] in h by A5,FUNCT_1:8;
end;
hereby let y; assume y in Y;
then consider x such that
A6: x in dom h & y = h.x by A3,FUNCT_1:def 5;
take x;
thus x in X & [x,y] in h by A6,FUNCT_1:8;
end;
let x,y,z,u; assume
[x,y] in h & [z,u] in h;
then x in dom h & y = h.x & z in dom h & u = h.z by FUNCT_1:8;
hence x = z iff y = u by A2,FUNCT_1:def 8;
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 Th12;
hence thesis by Th13;
end;
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;
coherence proof
f.x is Element of L;
hence thesis;
end;
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
:Def6: 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
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
(ex z being set,S being T-Sequence
st z = last S & dom S = succ O & S.{} = 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 <> {} & C is_limit_ordinal
holds S.C = D(C,S|C) ) &
for x1,x2 being set st
(ex L0 being T-Sequence st x1 = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) ) &
(ex L0 being T-Sequence st x2 = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal holds L0.C = D(C,L0|C) )
holds x1 = x2 from TS_Def;
hence thesis;
end;
func (f, O)-.x means
:Def7: 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
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
(ex z being set,S being T-Sequence
st z = last S & dom S = succ O & S.{} = 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 <> {} & C is_limit_ordinal
holds S.C = D(C,S|C) ) &
for x1,x2 being set st
(ex L0 being T-Sequence st x1 = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal holds L0.C = D(C,L0|C) ) &
(ex L0 being T-Sequence st x2 = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) )
holds x1 = x2 from TS_Def;
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 T-Sequence;
canceled;
theorem Th16:
(f, {})+.x = x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
A1:
for O being Ordinal, y being set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
thus F({}) = x from TS_Result0(A1);
end;
theorem Th17:
(f, {})-.x = x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
A1:
for O being Ordinal, y being set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def7;
thus F({}) = x from TS_Result0(A1);
end;
theorem Th18:
(f, succ O)+.x = f.(f, O)+.x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
A1:
for O being Ordinal, y being set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
for O being Ordinal holds F(succ O) = C(O,F(O))
from TS_ResultS(A1);
hence thesis;
end;
theorem Th19:
(f, succ O)-.x = f.(f, O)-.x
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
A1:
for O being Ordinal, y being set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def7;
for O being Ordinal holds F(succ O) = C(O,F(O))
from TS_ResultS(A1);
hence thesis;
end;
theorem Th20:
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)
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
deffunc F(Ordinal)=(f, $1)+.x;
assume that
A1: O <> {} & 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 set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
thus F(O) = D(O,T) from TS_ResultL(A4, A1, A2, A3);
end;
theorem Th21:
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)
proof
deffunc C(Ordinal,set)=f.$2;
deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
deffunc F(Ordinal)=(f, $1)-.x;
assume that
A1: O <> {} & 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 set holds y = F(O) iff
ex L0 being T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = 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 <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def7;
thus F(O) = D(O,T) from TS_ResultL(A4, A1, A2, A3);
end;
theorem
iter(f, n).x = (f, n)+.x
proof
A1: dom f = the carrier of L by FUNCT_2:def 1;
then A2: x in dom f \/ rng f by XBOOLE_0:def 2;
defpred P[Nat] means iter(f, $1).x = (f, $1)+.x;
iter(f, 0).x = id(dom f \/ rng f).x by FUNCT_7:70
.= x by A2,FUNCT_1:35
.= (f, 0)+.x by Th16; then A3: P[0];
A4: now let n be Nat; assume
A5: P[n];
rng f c= the carrier of L by RELSET_1:12;
then A6: dom iter(f, n) = dom f by A1,FUNCT_7:76;
iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:73
.= f.(f, n)+.x by A1,A5,A6,FUNCT_1:23
.= (f, succ n)+.x by Th18
.= (f, n+1)+.x by CARD_1:52;
hence P[n+1];
end;
for n being Nat holds P[n] from Ind(A3, A4);
hence iter(f, n).x = (f, n)+.x;
end;
theorem
iter(f, n).x = (f, n)-.x
proof
A1: dom f = the carrier of L by FUNCT_2:def 1;
then A2: x in dom f \/ rng f by XBOOLE_0:def 2;
defpred P[Nat] means iter(f, $1).x = (f, $1)-.x;
iter(f, 0).x = id(dom f \/ rng f).x by FUNCT_7:70
.= x by A2,FUNCT_1:35
.= (f, 0)-.x by Th17; then A3: P[0];
A4: now let n be Nat; assume
A5: P[n];
rng f c= the carrier of L by RELSET_1:12;
then A6: dom iter(f, n) = dom f by A1,FUNCT_7:76;
iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:73
.= f.(f, n)-.x by A1,A5,A6,FUNCT_1:23
.= (f, succ n)-.x by Th19
.= (f, n+1)-.x by CARD_1:52;
hence P[n+1];
end;
for n being Nat holds P[n] from Ind(A3, A4);
hence iter(f, n).x = (f, n)-.x;
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;
coherence proof
defpred P[Ordinal] means (f, $1)+.a is Element of L;
(f, {})+.a = a by Th16;
then A1: P[{}];
A2: now let O1; assume P[O1];
then reconsider fa = (f, O1)+.a as Element of L;
f.fa = (f, succ O1)+.a by Th18;
hence P[succ O1];
end;
deffunc F(Ordinal)=(f, $1)+.a;
A3: now let O1; assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 st O2 in O1 holds P[O2];
consider Ls being T-Sequence such that
A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
from TS_Lambda;
(f, O1)+.a = "\/"(rng Ls, L) by A4,A5,Th20;
hence P[O1];
end;
for O holds P[O] from Ordinal_Ind(A1, A2, A3);
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;
coherence proof
defpred P[Ordinal] means (f, $1)-.a is Element of L;
(f, {})-.a = a by Th17;
then A1: P[{}];
A2: now let O1; assume P[O1];
then reconsider fa = (f, O1)-.a as Element of L;
f.fa = (f, succ O1)-.a by Th19;
hence P[succ O1];
end;
deffunc F(Ordinal)=(f, $1)-.a;
A3: now let O1; assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 st O2 in O1 holds P[O2];
consider Ls being T-Sequence such that
A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 =F(O2)
from TS_Lambda;
(f, O1)-.a = "/\"(rng Ls, L) by A4,A5,Th21;
hence P[O1];
end;
for O holds P[O] from Ordinal_Ind(A1, A2, A3);
hence thesis;
end;
end;
definition
let L be non empty LattStr, P be Subset of L;
attr P is with_suprema means
:Def8:
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
:Def9:
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;
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 & y in P;
take z = x"\/"y;
thus z in P;
thus x [= z & y [= z by LATTICES:22;
let z' be Element of L; assume z' in P & x [= z' & y [= z';
hence z [= z' by BOOLEALG:11;
end;
let x,y be Element of L such that x in P & y in P;
take z = x"/\"y;
thus z in P;
thus z [= x & z [= y by LATTICES:23;
let z' be Element of L; assume z' in P & z' [= x & z' [= y;
hence z' [= z by BOOLEALG:12;
end;
end;
definition
let L be Lattice,
P be non empty with_suprema with_infima Subset of L;
func latt P -> strict Lattice means
:Def10:
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');
existence proof
set LL = LattRel L;
set cL = the carrier of L;
set LR = LL|_2 P;
LR c= [:P, P:] by WELLORD1:15;
then reconsider LR as Relation of P by RELSET_1:def 1;
field LL = cL by FILTER_1:33;
then
A1: LL is_reflexive_in cL & LL is_antisymmetric_in cL &
LL is_transitive_in cL by RELAT_2:def 9,def 12,def 16;
A2: field LR = P proof
thus field LR c= P by WELLORD1:20;
let x be set;
assume A3: x in P;
then A4: [x,x] in [:P, P:] by ZFMISC_1:106;
A5: [x,x] in LL by A1,A3,RELAT_2:def 1;
LR = LL /\ [:P, P:] by WELLORD1:def 6;
then [x, x] in LR by A4,A5,XBOOLE_0:def 3;
hence x in field LR by RELAT_1:30;
end;
LR is reflexive by WELLORD1:22;
then A6: LR is_reflexive_in P by A2,RELAT_2:def 9;
LR is antisymmetric by WELLORD1:25;
then A7: LR is_antisymmetric_in P by A2,RELAT_2:def 12;
LR is transitive by WELLORD1:24;
then A8: LR is_transitive_in P by A2,RELAT_2:def 16;
dom LR = P by A6,ORDERS_1:98;
then LR is total by PARTFUN1:def 4;
then reconsider LR as Order of P
by A2,A6,A7,A8,RELAT_2:def 9,def 12,def 16;
set RS = RelStr(#P, LR#);
A9: 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
A10: zL in P & xL [= zL & yL [= zL &
for z' being Element of L st z' in P & xL [= z' & yL [= z'
holds zL [= z' by Def8;
reconsider z = zL as Element of RS by A10;
take z;
[xL,zL] in [:P,P:] & [yL,zL] in [:P,P:] &
[xL,zL] in LL & [yL,zL] in LL by A10,FILTER_1:32,ZFMISC_1:106;
then [xL,zL] in LR & [yL,zL] in LR by WELLORD1:16;
hence x <= z & y <= z by ORDERS_1:def 9;
let z' be Element of RS; assume
A11: x <= z' & y <= z';
z' in P; then reconsider z'L = z' as Element of L;
[x,z'] in LR & [y,z'] in LR by A11,ORDERS_1:def 9;
then [x,z'] in LL & [y,z'] in LL by WELLORD1:16;
then xL [= z'L & yL [= z'L by FILTER_1:32;
then zL [= z'L by A10;
then [zL,z'L] in [:P, P:] & [zL,z'L] in LL
by A10,FILTER_1:32,ZFMISC_1:106;
then [zL,z'L] in LR by WELLORD1:16;
hence z <= z' by ORDERS_1:def 9;
end;
A12: 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
A13: zL in P & zL [= xL & zL [= yL &
for z' being Element of L st z' in P & z' [= xL & z' [= yL
holds z' [= zL by Def9;
reconsider z = zL as Element of RS by A13;
take z;
[zL,xL] in [:P,P:] & [zL,yL] in [:P,P:] &
[zL,xL] in LL & [zL,yL] in LL by A13,FILTER_1:32,ZFMISC_1:106;
then [zL,xL] in LR & [zL,yL] in LR by WELLORD1:16;
hence z <= x & z <= y by ORDERS_1:def 9;
let z' be Element of RS; assume
A14: z' <= x & z' <= y;
z' in P; then reconsider z'L = z' as Element of L;
[z',x] in LR & [z',y] in LR by A14,ORDERS_1:def 9;
then [z',x] in LL & [z',y] in LL by WELLORD1:16;
then z'L [= xL & z'L [= yL by FILTER_1:32;
then z'L [= zL by A13;
then [z'L,zL] in [:P, P:] & [z'L,zL] in LL
by A13,FILTER_1:32,ZFMISC_1:106;
then [z'L,zL] in LR by WELLORD1:16;
hence z' <= z by ORDERS_1:def 9;
end;
A15: RS is Poset by A6,A7,A8,ORDERS_1:def 4,def 5,def 6;
take IT = latt RS;
A16: LattPOSet IT = RelStr(#the carrier of IT, LattRel IT#) by LATTICE3:def 2;
A17: RS = LattPOSet IT by A9,A12,A15,LATTICE3:def 15;
thus
the carrier of IT = P by A9,A12,A15,A16,LATTICE3:def 15;
let x, y be Element of IT;
x in P & y in P by A16,A17;
then reconsider x' = x, y' = y as Element of L;
take x', y';
thus x = x' & y = y';
hereby assume x [= y;
then [x, y] in LR by A16,A17,FILTER_1:32;
then [x, y] in LattRel L by WELLORD1:16;
hence x' [= y' by FILTER_1:32;
end;
A18: [x, y] in [:P, P:] by A16,A17,ZFMISC_1:106;
assume x' [= y';
then [x, y] in LattRel L by FILTER_1:32;
then [x, y] in LattRel IT by A16,A17,A18,WELLORD1:16;
hence x [= y by FILTER_1:32;
end;
uniqueness proof
let it1, it2 be strict Lattice such that
A19: the carrier of it1 = P &
for x, y being Element of it1 ex x', y' being Element of L st x = x' & y = y'
& (x [= y iff x' [= y') and
A20: the carrier of it2 = P &
for x, y being Element of it2 ex x', y' being Element of L st x = x' & y = y'
& (x [= y iff x' [= y');
A21: LattPOSet it1 = RelStr(#the carrier of it1,LattRel it1#)
by LATTICE3:def 2;
A22: LattPOSet it2 = RelStr(#the carrier of it2,LattRel it2#)
by LATTICE3:def 2;
A23: LattRel it1 = { [p,q] where p is Element of it1,
q is Element of it1: p [= q }
by FILTER_1:def 8;
A24: LattRel it2 = { [p,q] where p is Element of it2,
q is Element of it2: p [= q }
by FILTER_1:def 8;
now let a be set;
hereby assume a in LattRel it1;
then consider p1, q1 being Element of it1 such that
A25: a = [p1, q1] & p1 [= q1 by A23;
reconsider p1, q1 as Element of it1;
consider pl1, ql1 being Element of L such that
A26: p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1) by A19;
reconsider p2 = p1, q2 = q1 as Element of it2 by A19,A20;
consider pl2, ql2 being Element of L such that
A27: p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A20;
thus a in LattRel it2 by A24,A25,A26,A27;
end;
assume a in LattRel it2;
then consider p1, q1 being Element of it2 such that
A28: a = [p1, q1] & p1 [= q1 by A24;
reconsider p1, q1 as Element of it2;
consider pl1, ql1 being Element of L such that
A29: p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1) by A20;
reconsider p2 = p1, q2 = q1 as Element of it1 by A19,A20;
consider pl2, ql2 being Element of L such that
A30: p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A19;
thus a in LattRel it1 by A23,A28,A29,A30;
end;
then LattRel it1 = LattRel it2 by TARSKI:2;
hence it1 = it2 by A19,A20,A21,A22,LATTICE3:6;
end;
end;
begin :: Complete lattices ::::::::::::::::::::::::::::::::::::::::::::::::
definition
cluster complete -> bounded Lattice;
coherence proof let L be Lattice; assume L is complete;
then L is 0_Lattice & L is 1_Lattice by LATTICE3:50,51;
hence L is bounded by LATTICES:def 15;
end;
end;
reserve L for complete Lattice,
f for (monotone UnOp of L),
a, b for Element of L;
theorem Th24:
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 a be Element of L; assume a in H;
then consider h being Element of L such that
A1: a = h & h [= f.h;
reconsider fh = f.h as Element of L;
take fh;
thus a [= fh & fh in fH by A1;
end;
then A2: uH [= fuH by LATTICE3:48;
now let fh be Element of L; assume fh in fH;
then consider h being Element of L such that
A3: fh = f.h & h [= f.h;
h in H by A3;
then h [= uH by LATTICE3:38;
hence fh [= f.uH by A3,QUANTAL1:def 12;
end;
then fH is_less_than f.uH by LATTICE3:def 17;
then fuH [= f.uH by LATTICE3:def 21;
then A4: uH [= f.uH by A2,LATTICES:25;
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 A4,LATTICES:26;
end;
theorem Th25:
for a st a [= f.a for O holds a [= (f, O)+.a
proof
let a; assume
A1: a [= f.a;
defpred S[Ordinal] means a [= (f, $1)+.a;
A2: S[{}] by Th16;
A3: now let O1; assume S[O1];
then f.a [= f.((f, O1)+.a) by QUANTAL1:def 12;
then a [= f.((f, O1)+.a) by A1,LATTICES:25;
hence S[succ O1] by Th18;
end;
deffunc F(Ordinal)=(f, $1)+.a;
A4: now let O1; assume
A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
consider Ls being T-Sequence such that
A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
from TS_Lambda;
consider O2 being set such that
A7: O2 in O1 by A5,XBOOLE_0:def 1;
reconsider O2 as Ordinal by A7,ORDINAL1:23;
A8: Ls.O2 = (f, O2)+.a by A6,A7;
Ls.O2 in rng Ls by A6,A7,FUNCT_1:def 5;
then A9: (f, O2)+.a [= "\/"(rng Ls, L) by A8,LATTICE3:38;
S[O2] by A5,A7;
then a [= "\/"(rng Ls, L) by A9,LATTICES:25;
hence S[O1] by A5,A6,Th20;
end;
thus for O holds S[O] from Ordinal_Ind(A2, A3, A4);
end;
theorem Th26:
for a st f.a [= a for O holds (f, O)-.a [= a
proof
let a; assume
A1: f.a [= a;
defpred S[Ordinal] means (f, $1)-.a [= a;
A2: S[{}] by Th17;
A3: now let O1; assume S[O1];
then f.((f, O1)-.a) [= f.a by QUANTAL1:def 12;
then f.((f, O1)-.a) [= a by A1,LATTICES:25;
hence S[succ O1] by Th19;
end;
deffunc F(Ordinal)=(f, $1)-.a;
A4: now let O1; assume
A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
consider Ls being T-Sequence such that
A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
from TS_Lambda;
consider O2 being set such that
A7: O2 in O1 by A5,XBOOLE_0:def 1;
reconsider O2 as Ordinal by A7,ORDINAL1:23;
A8: Ls.O2 = (f, O2)-.a by A6,A7;
Ls.O2 in rng Ls by A6,A7,FUNCT_1:def 5;
then A9: "/\"(rng Ls, L) [= (f, O2)-.a by A8,LATTICE3:38;
S[O2] by A5,A7;
then "/\"(rng Ls, L) [= a by A9,LATTICES:25;
hence S[O1] by A5,A6,Th21;
end;
thus for O holds S[O] from Ordinal_Ind(A2, A3, A4);
end;
theorem Th27:
for a st a [= f.a
for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a
proof let a; assume
A1: a [= f.a;
defpred S[Ordinal] means
for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O1)+.a [= (f, O2)+.a;
A2: S[{}]
proof
let O1, O2; assume A3: O1 c= O2 & O2 c= {};
then O2 = {} by XBOOLE_1:3;
hence (f, O1)+.a [= (f, O2)+.a by A3,XBOOLE_1:3;
end;
A4: now let O4; assume A5: S[O4];
thus S[succ O4]
proof
let O1, O2; assume
A6: O1 c= O2 & O2 c= succ O4;
per cases;
suppose O1 = O2 & O2 <> succ O4;
hence (f, O1)+.a [= (f, O2)+.a;
suppose O1 <> O2 & O2 <> succ O4;
then O2 c< succ O4 by A6,XBOOLE_0:def 8;
then O2 in succ O4 by ORDINAL1:21;
then O2 c= O4 by ORDINAL1:34;
hence (f, O1)+.a [= (f, O2)+.a by A5,A6;
suppose O1 = O2 & O2 = succ O4;
hence (f, O1)+.a [= (f, O2)+.a;
suppose A7: O1 <> O2 & O2 = succ O4;
then O1 c< O2 by A6,XBOOLE_0:def 8;
then A8: O1 in O2 by ORDINAL1:21;
A9: (f, O4)+.a [= (f, succ O4)+.a proof
per cases by ORDINAL1:42;
suppose A10: O4 is_limit_ordinal;
thus thesis proof
per cases;
suppose O4 = {};
then (f, O4)+.a = a by Th16;
hence thesis by A1,Th18;
suppose A11: O4 <> {};
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being T-Sequence such that
A12: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
from TS_Lambda;
A13: (f, O4)+.a = "\/"(rng L1, L) by A10,A11,A12,Th20;
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 set such that
A14: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A14,ORDINAL1:23;
O3 c= O4 by A12,A14,ORDINAL1:def 2;
then (f, O3)+.a [= (f, O4)+.a by A5;
then f.(f, O3)+.a [= f.(f, O4)+.a by QUANTAL1:def 12;
then (f, succ O3)+.a [= f.(f, O4)+.a by Th18;
then A15: (f, succ O3)+.a [= (f, succ O4)+.a by Th18;
A16: succ O3 c= O4 by A12,A14,ORDINAL1:33;
O3 in succ O3 by ORDINAL1:10;
then O3 c= succ O3 by ORDINAL1:def 2;
then A17: (f, O3)+.a [= (f, succ O3)+.a by A5,A16;
q = (f, O3)+.a by A12,A14;
hence q [= (f, succ O4)+.a by A15,A17,LATTICES:25;
end;
hence thesis by A13,LATTICE3:def 21;
end;
suppose ex O3 st O4 = succ O3; then consider O3 such that
A18: O4 = succ O3;
succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
then O3 c= O4 by A18,XBOOLE_1:7;
then (f, O3)+.a [= (f, O4)+.a by A5;
then f.((f, O3)+.a) [= f.((f, O4)+.a) by QUANTAL1:def 12;
then (f, O4)+.a [= f.((f, O4)+.a) by A18,Th18;
hence thesis by Th18;
end;
O1 c= O4 by A7,A8,ORDINAL1:34;
then (f, O1)+.a [= (f, O4)+.a by A5;
hence (f, O1)+.a [= (f, O2)+.a by A7,A9,LATTICES:25;
end;
end;
A19: now let O4; assume
A20: O4 <> {} & O4 is_limit_ordinal & for O3 st O3 in O4 holds S[O3];
thus S[O4]
proof
let O1, O2; assume
A21: O1 c= O2 & O2 c= O4;
A22: O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A23: O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
per cases by A21,A22,ORDINAL1:21;
suppose A24: O2 = O4;
thus (f, O1)+.a [= (f, O2)+.a proof
per cases by A21,A23,ORDINAL1:21;
suppose O1 = O2;
hence thesis;
suppose A25: O1 in O2;
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being T-Sequence such that
A26: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
from TS_Lambda;
A27: (f, O2)+.a = "\/"(rng L1, L) by A20,A24,A26,Th20;
L1.O1 = (f, O1)+.a & L1.O1 in rng L1 by A25,A26,FUNCT_1:def 5;
hence thesis by A27,LATTICE3:38;
end;
suppose O2 in O4;
hence (f, O1)+.a [= (f, O2)+.a by A20,A21;
end;
end;
A28: for O4 holds S[O4] from Ordinal_Ind(A2, A4, A19);
let O1, O2; assume O1 c= O2;
hence (f, O1)+.a [= (f, O2)+.a by A28;
end;
theorem Th28:
for a st f.a [= a
for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a
proof let a; assume
A1: f.a [= a;
defpred S[Ordinal] means
for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O2)-.a [= (f, O1)-.a;
A2: S[{}]
proof
let O1, O2; assume A3: O1 c= O2 & O2 c= {};
then O2 = {} by XBOOLE_1:3;
hence (f, O2)-.a [= (f, O1)-.a by A3,XBOOLE_1:3;
end;
A4: now let O4; assume
A5: S[O4];
thus S[succ O4]
proof
let O1, O2; assume
A6: O1 c= O2 & O2 c= succ O4;
per cases;
suppose O1 = O2 & O2 <> succ O4;
hence (f, O2)-.a [= (f, O1)-.a;
suppose O1 <> O2 & O2 <> succ O4;
then O2 c< succ O4 by A6,XBOOLE_0:def 8;
then O2 in succ O4 by ORDINAL1:21;
then O2 c= O4 by ORDINAL1:34;
hence (f, O2)-.a [= (f, O1)-.a by A5,A6;
suppose O1 = O2 & O2 = succ O4;
hence (f, O2)-.a [= (f, O1)-.a;
suppose A7: O1 <> O2 & O2 = succ O4;
then O1 c< O2 by A6,XBOOLE_0:def 8;
then A8: O1 in O2 by ORDINAL1:21;
A9: (f, succ O4)-.a [= (f, O4)-.a proof
per cases by ORDINAL1:42;
suppose A10: O4 is_limit_ordinal;
thus thesis proof
per cases;
suppose O4 = {};
then (f, O4)-.a = a by Th17;
hence thesis by A1,Th19;
suppose A11: O4 <> {};
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being T-Sequence such that
A12: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
from TS_Lambda;
A13: (f, O4)-.a = "/\"(rng L1, L) by A10,A11,A12,Th21;
(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 set such that
A14: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A14,ORDINAL1:23;
O3 c= O4 by A12,A14,ORDINAL1:def 2;
then (f, O4)-.a [= (f, O3)-.a by A5;
then f.(f, O4)-.a [= f.(f, O3)-.a by QUANTAL1:def 12;
then (f, succ O4)-.a [= f.(f, O3)-.a by Th19;
then A15: (f, succ O4)-.a [= (f, succ O3)-.a by Th19;
A16: succ O3 c= O4 by A12,A14,ORDINAL1:33;
O3 in succ O3 by ORDINAL1:10;
then O3 c= succ O3 by ORDINAL1:def 2;
then A17: (f, succ O3)-.a [= (f, O3)-.a by A5,A16;
q = (f, O3)-.a by A12,A14;
hence (f, succ O4)-.a [= q by A15,A17,LATTICES:25;
end;
hence thesis by A13,LATTICE3:34;
end;
suppose ex O3 st O4 = succ O3; then consider O3 such that
A18: O4 = succ O3;
succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
then O3 c= O4 by A18,XBOOLE_1:7;
then (f, O4)-.a [= (f, O3)-.a by A5;
then f.((f, O4)-.a) [= f.((f, O3)-.a) by QUANTAL1:def 12;
then f.((f, O4)-.a) [= (f, O4)-.a by A18,Th19;
hence thesis by Th19;
end;
O1 c= O4 by A7,A8,ORDINAL1:34;
then (f, O4)-.a [= (f, O1)-.a by A5;
hence (f, O2)-.a [= (f, O1)-.a by A7,A9,LATTICES:25;
end;
end;
A19: now let O4; assume
A20: O4 <> {} & O4 is_limit_ordinal & for O3 st O3 in O4 holds S[O3];
thus S[O4]
proof
let O1, O2; assume
A21: O1 c= O2 & O2 c= O4;
A22: O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A23: O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
per cases by A21,A22,ORDINAL1:21;
suppose A24: O2 = O4;
thus (f, O2)-.a [= (f, O1)-.a proof
per cases by A21,A23,ORDINAL1:21;
suppose O1 = O2;
hence thesis;
suppose A25: O1 in O2;
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being T-Sequence such that
A26: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
from TS_Lambda;
A27: (f, O2)-.a = "/\"(rng L1, L) by A20,A24,A26,Th21;
L1.O1 = (f, O1)-.a & L1.O1 in rng L1 by A25,A26,FUNCT_1:def 5;
hence thesis by A27,LATTICE3:38;
end;
suppose O2 in O4;
hence (f, O2)-.a [= (f, O1)-.a by A20,A21;
end;
end;
A28: for O4 holds S[O4] from Ordinal_Ind(A2, A4, A19);
let O1, O2; assume O1 c= O2;
hence (f, O2)-.a [= (f, O1)-.a by A28;
end;
theorem Th29:
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; assume
A2: O1 c< O2 & not (f, O2)+.a is_a_fixpoint_of f &
(f, O1)+.a = (f, O2)+.a;
then O1 in O2 by ORDINAL1:21;
then succ O1 c= O2 by ORDINAL1:33;
then A3: (f, succ O1)+.a [= (f, O2)+.a by A1,Th27;
succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
then O1 c= succ O1 by XBOOLE_1:7;
then (f, O1)+.a [= (f, succ O1)+.a by A1,Th27;
then (f, O1)+.a = (f, succ O1)+.a by A2,A3,LATTICES:26;
then (f, O1)+.a = f.(f, O1)+.a by Th18;
hence contradiction by A2,Def2;
end;
theorem Th30:
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; assume
A2: O1 c< O2 & not (f, O2)-.a is_a_fixpoint_of f &
(f, O1)-.a = (f, O2)-.a;
then O1 in O2 by ORDINAL1:21;
then succ O1 c= O2 by ORDINAL1:33;
then A3: (f, O2)-.a [= (f, succ O1)-.a by A1,Th28;
succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
then O1 c= succ O1 by XBOOLE_1:7;
then (f, succ O1)-.a [= (f, O1)-.a by A1,Th28;
then (f, O1)-.a = (f, succ O1)-.a by A2,A3,LATTICES:26;
then (f, O1)-.a = f.(f, O1)-.a by Th19;
hence contradiction by A2,Def2;
end;
theorem Th31:
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
A1: a [= f.a & (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;
A2: S[{}] by XBOOLE_1:3;
A3: now let O2; assume
A4: S[O2];
thus S[succ O2]
proof
assume
A5: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence fa = (f, succ O2)+.a;
suppose O1 <> succ O2;
then O1 c< succ O2 by A5,XBOOLE_0:def 8;
then O1 in succ O2 by ORDINAL1:21;
hence fa = f.(f, O2)+.a by A1,A4,Def1,ORDINAL1:34
.= (f, succ O2)+.a by Th18;
end;
end;
A6: now let O2; assume
A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds S[O3];
thus S[O2]
proof
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being T-Sequence such that
A8: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
from TS_Lambda;
A9: (f, O2)+.a = "\/"(rng L1, L) by A7,A8,Th20;
rng L1 is_less_than fa proof
let q be Element of L; assume q in rng L1;
then consider O3 being set such that
A10: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A10,ORDINAL1:23;
per cases;
suppose O1 c= O3;
then (f, O3)+.a [= fa by A7,A8,A10;
hence q [= fa by A8,A10;
suppose O3 c= O1;
then (f, O3)+.a [= fa by A1,Th27;
hence q [= fa by A8,A10;
end;
then A11: (f, O2)+.a [= fa by A9,LATTICE3:def 21;
assume O1 c= O2; then fa [= (f, O2)+.a by A1,Th27;
hence fa = (f, O2)+.a by A11,LATTICES:26;
end;
end;
thus for O2 holds S[O2] from Ordinal_Ind(A2, A3, A6);
end;
theorem Th32:
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
A1: f.a [= a & (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;
A2: S[{}] by XBOOLE_1:3;
A3: now let O2; assume
A4: S[O2];
thus S[succ O2]
proof
assume
A5: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence fa = (f, succ O2)-.a;
suppose O1 <> succ O2;
then O1 c< succ O2 by A5,XBOOLE_0:def 8;
then O1 in succ O2 by ORDINAL1:21;
hence fa = f.(f, O2)-.a by A1,A4,Def1,ORDINAL1:34
.= (f, succ O2)-.a by Th19;
end;
end;
A6: now let O2; assume
A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds S[O3];
thus S[O2]
proof
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being T-Sequence such that
A8: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
from TS_Lambda;
A9: (f, O2)-.a = "/\"(rng L1, L) by A7,A8,Th21;
fa is_less_than rng L1 proof
let q be Element of L; assume q in rng L1;
then consider O3 being set such that
A10: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A10,ORDINAL1:23;
per cases;
suppose O1 c= O3;
then fa [= (f, O3)-.a by A7,A8,A10;
hence fa [= q by A8,A10;
suppose O3 c= O1;
then fa [= (f, O3)-.a by A1,Th28;
hence fa [= q by A8,A10;
end;
then A11: fa [= (f, O2)-.a by A9,LATTICE3:40;
assume O1 c= O2; then (f, O2)-.a [= fa by A1,Th28;
hence fa = (f, O2)-.a by A11,LATTICES:26;
end;
end;
thus for O2 holds S[O2] from Ordinal_Ind(A2, A3, A6);
end;
Lm1: :: trzeba przenisc do ORDINAL1
O1 c< O2 or O1 = O2 or O2 c< O1
proof assume not(O1 c< O2 or O1 = O2 or O2 c< O1);
then not(O1 c= O2 or O2 c= O1) by XBOOLE_0:def 8;
hence contradiction;
end;
theorem Th33:
for a st a [= f.a
ex O st Card O <=` Card the carrier of L & (f, O)+.a is_a_fixpoint_of f
proof let a; assume
A1: a [= f.a;
set cL = the carrier of L; set ccL = Card cL; set nccL = nextcard ccL;
deffunc F(Ordinal)=(f, $1)+.a;
consider Ls being T-Sequence such that
A2: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(O2)
from TS_Lambda;
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 set; assume
A5: x1 in dom Ls & x2 in dom Ls & Ls.x1 = Ls.x2;
then reconsider x1, x2 as Ordinal by ORDINAL1:23;
A6: Ls.x1 = (f, x1)+.a & Ls.x2 = (f, x2)+.a by A2,A5;
per cases by Lm1;
suppose A7: x1 c< x2;
not (f, x2)+.a is_a_fixpoint_of f by A2,A3,A5;
hence thesis by A1,A5,A6,A7,Th29;
suppose A8: x2 c< x1;
not (f, x1)+.a is_a_fixpoint_of f by A2,A3,A5;
hence thesis by A1,A5,A6,A8,Th29;
suppose x2 = x1;
hence thesis;
end;
rng Ls c= cL proof let y be set; assume y in rng Ls;
then consider x being set such that
A9: x in dom Ls & Ls.x = y by FUNCT_1:def 5;
reconsider x as Ordinal by A9,ORDINAL1:23;
Ls.x = (f, x)+.a by A2,A9;
hence y in cL by A9;
end;
then Card nccL <=` ccL by A2,A4,CARD_1:26;
then nccL <=` ccL & ccL <` nccL by CARD_1:32,def 5;
hence contradiction by CARD_1:14;
end;
then consider O such that
A10: O in nccL & (f, O)+.a is_a_fixpoint_of f;
take O;
Card O <` nccL by A10,CARD_1:25;
hence Card O <=` Card cL by CARD_4:23;
thus (f, O)+.a is_a_fixpoint_of f by A10;
end;
theorem Th34:
for a st f.a [= a
ex O st Card O <=` Card the carrier of L & (f, O)-.a is_a_fixpoint_of f
proof let a; assume
A1: f.a [= a;
set cL = the carrier of L; set ccL = Card cL; set nccL = nextcard ccL;
deffunc F(Ordinal)=(f, $1)-.a;
consider Ls being T-Sequence such that
A2: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(O2)
from TS_Lambda;
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 set; assume
A5: x1 in dom Ls & x2 in dom Ls & Ls.x1 = Ls.x2;
then reconsider x1, x2 as Ordinal by ORDINAL1:23;
A6: Ls.x1 = (f, x1)-.a & Ls.x2 = (f, x2)-.a by A2,A5;
per cases by Lm1;
suppose A7: x1 c< x2;
not (f, x2)-.a is_a_fixpoint_of f by A2,A3,A5;
hence thesis by A1,A5,A6,A7,Th30;
suppose A8: x2 c< x1;
not (f, x1)-.a is_a_fixpoint_of f by A2,A3,A5;
hence thesis by A1,A5,A6,A8,Th30;
suppose x2 = x1;
hence thesis;
end;
rng Ls c= cL proof let y be set; assume y in rng Ls;
then consider x being set such that
A9: x in dom Ls & Ls.x = y by FUNCT_1:def 5;
reconsider x as Ordinal by A9,ORDINAL1:23;
Ls.x = (f, x)-.a by A2,A9;
hence y in cL by A9;
end;
then Card nccL <=` ccL by A2,A4,CARD_1:26;
then nccL <=` ccL & ccL <` nccL by CARD_1:32,def 5;
hence contradiction by CARD_1:14;
end;
then consider O such that
A10: O in nccL & (f, O)-.a is_a_fixpoint_of f;
take O;
Card O <` nccL by A10,CARD_1:25;
hence Card O <=` Card cL by CARD_4:23;
thus (f, O)-.a is_a_fixpoint_of f by A10;
end;
theorem Th35:
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)
proof let a, b; assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then A1: a = f.a & b = f.b by Def1;
reconsider ab = a"\/"b as Element of L;
A2: a [= ab & b [= ab by LATTICES:22;
then f.a [= f.ab & f.b [= f.ab by QUANTAL1:def 12;
then A3: ab [= f.ab by A1,FILTER_0:6;
then consider O such that
A4: Card O <=` Card the carrier of L &
(f, O)+.ab is_a_fixpoint_of f by Th33;
take O;
thus Card O <=` Card the carrier of L &
(f, O)+.(a"\/"b) is_a_fixpoint_of f by A4;
A5: ab [= (f, O)+.(a"\/"b) by A3,Th25;
hence a [= (f, O)+.(a"\/"b) by A2,LATTICES:25;
thus b [= (f, O)+.(a"\/"b) by A2,A5,LATTICES:25;
end;
theorem Th36:
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
proof let a, b; assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then A1: a = f.a & b = f.b by Def1;
reconsider ab = a"/\"b as Element of L;
A2: ab [= a & ab [= b by LATTICES:23;
then f.ab [= f.a & f.ab [= f.b by QUANTAL1:def 12;
then A3: f.ab [= ab by A1,FILTER_0:7;
then consider O such that
A4: Card O <=` Card the carrier of L &
(f, O)-.ab is_a_fixpoint_of f by Th34;
take O;
thus Card O <=` Card the carrier of L &
(f, O)-.(a"/\"b) is_a_fixpoint_of f by A4;
A5: (f, O)-.(a"/\"b) [= ab by A3,Th26;
hence (f, O)-.(a"/\"b) [= a by A2,LATTICES:25;
thus (f, O)-.(a"/\"b) [= b by A2,A5,LATTICES:25;
end;
theorem Th37:
a [= f.a & a [= b & b is_a_fixpoint_of f
implies for O2 holds (f, O2)+.a [= b
proof assume
A1: a [= f.a & a [= b & b is_a_fixpoint_of f;
then A2: f.b = b by Def1;
defpred S[Ordinal] means (f, $1)+.a [= b;
A3: S[{}] by A1,Th16;
A4: now let O1; assume S[O1];
then f.(f, O1)+.a [= f.b by QUANTAL1:def 12;
hence S[succ O1] by A2,Th18;
end;
A5: now let O1; assume
A6: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
deffunc F(Ordinal)=(f, $1)+.a;
consider L1 being T-Sequence such that
A7: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
from TS_Lambda;
A8: (f, O1)+.a = "\/"(rng L1, L) by A6,A7,Th20;
rng L1 is_less_than b proof
let q be Element of L; assume q in rng L1;
then consider O3 being set such that
A9: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A9,ORDINAL1:23;
(f, O3)+.a [= b by A6,A7,A9;
hence q [= b by A7,A9;
end;
hence S[O1] by A8,LATTICE3:def 21;
end;
thus for O2 holds S[O2] from Ordinal_Ind(A3, A4, A5);
end;
theorem Th38:
f.a [= a & b [= a & b is_a_fixpoint_of f
implies for O2 holds b [= (f, O2)-.a
proof
assume
A1: f.a [= a & b [= a & b is_a_fixpoint_of f;
then A2: f.b = b by Def1;
defpred S[Ordinal] means b [= (f, $1)-.a;
A3: S[{}] by A1,Th17;
A4: now let O1; assume S[O1];
then f.b [= f.(f, O1)-.a by QUANTAL1:def 12;
hence S[succ O1] by A2,Th19;
end;
A5: now let O1; assume
A6: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
deffunc F(Ordinal)=(f, $1)-.a;
consider L1 being T-Sequence such that
A7: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
from TS_Lambda;
A8: (f, O1)-.a = "/\"(rng L1, L) by A6,A7,Th21;
b is_less_than rng L1 proof
let q be Element of L; assume q in rng L1;
then consider O3 being set such that
A9: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
reconsider O3 as Ordinal by A9,ORDINAL1:23;
b [= (f, O3)-.a by A6,A7,A9;
hence b [= q by A7,A9;
end;
hence S[O1] by A8,LATTICE3:40;
end;
thus for O2 holds S[O2] from Ordinal_Ind(A3, 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
:Def11:
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]};
consider a being Element of L such that
A2: a is_a_fixpoint_of f by A1,Th24;
A3: a in P by A2;
P is Subset of L from SubsetD;
then reconsider P as Subset of L;
A4: P is with_suprema proof
let x,y be Element of L;assume A5: x in P & y in P;
then consider a being Element of L such that
A6: x = a & a is_a_fixpoint_of f;
consider b being Element of L such that
A7: y = b & b is_a_fixpoint_of f by A5;
reconsider a, b as Element of L;
reconsider ab = a"\/"b as Element of L;
consider O such that
A8: Card O <=` Card the carrier of L &
(f, O)+.ab is_a_fixpoint_of f &
a [= (f, O)+.ab & b [= (f, O)+.ab by A1,A6,A7,Th35;
set z = (f, O)+.ab;
take z;
thus z in P by A8;
thus x [= z & y [= z by A6,A7,A8;
let z' be Element of L; assume
A9: z' in P & x [= z' & y [= z';
then consider zz being Element of L such that
A10: zz = z' & zz is_a_fixpoint_of f;
A11: a = f.a & b = f.b by A6,A7,Def1;
a [= ab & b [= ab by LATTICES:22;
then f.a [= f.ab & f.b [= f.ab by A1,QUANTAL1:def 12;
then A12: ab [= f.ab by A11,FILTER_0:6;
ab [= z' by A6,A7,A9,FILTER_0:6;
hence z [= z' by A1,A10,A12,Th37;
end;
P is with_infima proof
let x,y be Element of L; assume A13: x in P & y in P;
then consider a being Element of L such that
A14: x = a & a is_a_fixpoint_of f;
consider b being Element of L such that
A15: y = b & b is_a_fixpoint_of f by A13;
reconsider a, b as Element of L;
reconsider ab = a"/\"b as Element of L;
consider O such that
A16: Card O <=` Card the carrier of L &
(f, O)-.ab is_a_fixpoint_of f &
(f, O)-.ab [= a & (f, O)-.ab [= b by A1,A14,A15,Th36;
set z = (f, O)-.ab;
take z;
thus z in P by A16;
thus z [= x & z [= y by A14,A15,A16;
let z' be Element of L; assume
A17: z' in P & z' [= x & z' [= y;
then consider zz being Element of L such that
A18: zz = z' & zz is_a_fixpoint_of f;
A19: a = f.a & b = f.b by A14,A15,Def1;
ab [= a & ab [= b by LATTICES:23;
then f.ab [= f.a & f.ab [= f.b by A1,QUANTAL1:def 12;
then A20: f.ab [= ab by A19,FILTER_0:7;
z' [= ab by A14,A15,A17,FILTER_0:7;
hence z' [= z by A1,A18,A20,Th38;
end;
then reconsider P as non empty with_suprema with_infima Subset of L
by A3,A4;
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 Th39:
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 Def11;
hence thesis by Def10;
end;
theorem Th40:
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 Th39;
let x be set; assume x in the carrier of FixPoints f;
then consider a such that
A2: x = a & a is_a_fixpoint_of f by A1;
thus x in the carrier of L by A2;
end;
theorem Th41:
(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 Th39;
hereby assume a in the carrier of FixPoints f; then consider b such that
A2: a = b & b is_a_fixpoint_of f by A1;
thus a is_a_fixpoint_of f by A2;
end;
assume a is_a_fixpoint_of f;
hence thesis by A1;
end;
theorem Th42:
for x, y being Element of FixPoints f, a, b
st x = a & y = b holds (x [= y iff a [= b)
proof
consider P being non empty with_suprema with_infima Subset of L such that
A1: P = {x where x is Element of L: x is_a_fixpoint_of f} &
FixPoints f = latt P by Def11;
let x, y be Element of FixPoints f, a, b; assume
A2: x = a & y = b;
consider a', b' being Element of L such that
A3: x = a' & y = b' & (x [= y iff a' [= b') by A1,Def10;
thus x [= y iff a [= b by A2,A3;
end;
theorem
FixPoints f is complete
proof
set F = FixPoints f;
set cF = the carrier of F;
set cL = the carrier of L;
A1: cF = {x where x is Element of L: x is_a_fixpoint_of f} by Th39;
let X be set;
set Y = X /\ cF;
A2: Y c= X & Y c= cF by XBOOLE_1:17;
set s = "\/"(Y, L);
Y is_less_than f.s proof
let q be Element of cL; assume
A3: q in Y;
then q [= s by LATTICE3:38;
then A4: f.q [= f.s by QUANTAL1:def 12;
reconsider q' = q as Element of L;
q' is_a_fixpoint_of f by A2,A3,Th41;
hence q [= f.s by A4,Def1;
end;
then A5: s [= f.s by LATTICE3:def 21;
then consider O such that
A6: Card O <=` Card cL & (f, O)+.s is_a_fixpoint_of f by Th33;
reconsider p' = (f, O)+.s as Element of L;
reconsider p = p' as Element of cF by A6,Th41;
reconsider p'' = p as Element of F;
take p;
thus X is_less_than p proof
let q be Element of cF; assume
A7: q in X;
reconsider q' = q as Element of F;
q in cF & cF c= cL by Th40;
then reconsider qL' = q as Element of L;
q in Y by A7,XBOOLE_0:def 3;
then A8: qL' [= s by LATTICE3:38;
s [= p' by A5,Th25;
then qL' [= p' by A8,LATTICES:25;
then q' [= p'' by Th42;
hence q [= p;
end;
let r be Element of cF such that
A9: X is_less_than r;
r in the carrier of F;
then consider r' being Element of L such that
A10: r' = r & r' is_a_fixpoint_of f by A1;
reconsider r'' = r as Element of F;
Y is_less_than r' proof
let q be Element of cL; assume
A11: q in Y;
then reconsider q'' = q as Element of F by A2;
reconsider q' = q as Element of L;
q'' [= r'' by A2,A9,A11,LATTICE3:def 17;
then q' [= r' by A10,Th42;
hence q [= r';
end;
then s [= r' by LATTICE3:def 21;
then p' [= r' by A5,A10,Th37;
then p'' [= r'' by A10,Th42;
hence p [= r;
end;
definition
let L, f;
func lfp f -> Element of L equals
:Def12: (f, nextcard the carrier of L)+.Bottom L;
coherence;
func gfp f -> Element of L equals
:Def13: (f, nextcard the carrier of L)-.Top L;
coherence;
end;
theorem Th44:
(lfp f is_a_fixpoint_of f) &
(ex O st Card O <=` 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:41;
then consider O such that
A2: Card O <=` Card the carrier of L and
A3: (f, O)+.Bottom L is_a_fixpoint_of f by Th33;
Card the carrier of L in nextcard the carrier of L by CARD_1:def 6;
then Card O in nextcard the carrier of L by A2,ORDINAL1:22;
then O in nextcard the carrier of L by CARD_3:60;
then O c= nextcard the carrier of L by ORDINAL1:def 2;
then A4: (f, O)+.Bottom L = (f, nextcard the carrier of L)+.Bottom
L by A1,A3,Th31;
hence lfp f is_a_fixpoint_of f by A3,Def12;
take O;
thus Card O <=` Card the carrier of L by A2;
thus thesis by A4,Def12;
end;
theorem Th45:
(gfp f is_a_fixpoint_of f) &
(ex O st Card O <=` 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:45;
then consider O such that
A2: Card O <=` Card the carrier of L and
A3: (f, O)-.Top L is_a_fixpoint_of f by Th34;
Card the carrier of L in nextcard the carrier of L by CARD_1:def 6;
then Card O in nextcard the carrier of L by A2,ORDINAL1:22;
then O in nextcard the carrier of L by CARD_3:60;
then O c= nextcard the carrier of L by ORDINAL1:def 2;
then A4: (f, O)-.Top L = (f, nextcard the carrier of L)-.Top L by A1,A3,Th32;
hence gfp f is_a_fixpoint_of f by A3,Def13;
take O;
thus Card O <=` Card the carrier of L by A2;
thus thesis by A4,Def13;
end;
theorem Th46:
a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f
proof assume
a is_a_fixpoint_of f;
then A1: f.a = a by Def1;
defpred S[Ordinal] means (f, $1)+.Bottom L [= a;
(f, {})+.Bottom L = Bottom L by Th16;
then A2: S[{}] by LATTICES:41;
A3: now let O1; assume S[O1];
then f.(f, O1)+.Bottom L [= f.a by QUANTAL1:def 12;
hence S[succ O1] by A1,Th18;
end;
A4: now let O1; assume
A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
deffunc F(Ordinal)=(f, $1)+.Bottom L;
consider L1 being T-Sequence such that
A6: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
from TS_Lambda;
A7: (f, O1)+.Bottom L = "\/"(rng L1, L) by A5,A6,Th20;
rng L1 is_less_than a proof
let q be Element of L; assume q in rng L1;
then consider C being set such that
A8: C in dom L1 & q = L1.C by FUNCT_1:def 5;
reconsider C as Ordinal by A8,ORDINAL1:23;
(f, C)+.Bottom L [= a by A5,A6,A8;
hence q [= a by A6,A8;
end;
hence S[O1] by A7,LATTICE3:def 21;
end;
A9: for O2 holds S[O2] from Ordinal_Ind(A2, A3, A4);
lfp f = (f, nextcard the carrier of L)+.Bottom L by Def12;
hence lfp f [= a by A9;
defpred S[Ordinal] means a [= (f, $1)-.Top L;
(f, {})-.Top L = Top L by Th17;
then A10: S[{}] by LATTICES:45;
A11: now let O1; assume S[O1];
then f.a [= f.(f, O1)-.Top L by QUANTAL1:def 12;
hence S[succ O1] by A1,Th19;
end;
A12: now let O1; assume
A13: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
deffunc F(Ordinal)=(f, $1)-.Top L;
consider L1 being T-Sequence such that
A14: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
from TS_Lambda;
A15: (f, O1)-.Top L = "/\"(rng L1, L) by A13,A14,Th21;
a is_less_than rng L1 proof
let q be Element of L; assume q in rng L1;
then consider C being set such that
A16: C in dom L1 & q = L1.C by FUNCT_1:def 5;
reconsider C as Ordinal by A16,ORDINAL1:23;
a [= (f, C)-.Top L by A13,A14,A16;
hence a [= q by A14,A16;
end;
hence S[O1] by A15,LATTICE3:40;
end;
A17: for O2 holds S[O2] from Ordinal_Ind(A10, A11, A12);
gfp f = (f, nextcard the carrier of L)-.Top L by Def13;
hence a [= gfp f by A17;
end;
theorem
f.a [= a implies lfp f [= a
proof assume
A1: f.a [= a;
then consider O such that
Card O <=` Card the carrier of L and
A2: (f, O)-.a is_a_fixpoint_of f by Th34;
A3: (f, O)-.a [= a by A1,Th26;
lfp f [= (f, O)-.a by A2,Th46;
hence lfp f [= a by A3,LATTICES:25;
end;
theorem
a [= f.a implies a [= gfp f
proof assume
A1: a [= f.a;
then consider O such that
Card O <=` Card the carrier of L and
A2: (f, O)+.a is_a_fixpoint_of f by Th33;
A3: a [= (f, O)+.a by A1,Th25;
(f, O)+.a [= gfp f by A2,Th46;
hence a [= gfp f by A3,LATTICES:25;
end;
begin :: Boolean Lattices
reserve f for (monotone UnOp of BooleLatt A);
definition
let A be set;
cluster BooleLatt A -> complete;
coherence by LATTICE3:25;
end;
theorem Th49:
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,QUANTAL1:def 12;
hence f.x c= f.y 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,Def3;
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
A1: 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 Th49;
take g;
reconsider lf = lfp f as Subset of A by LATTICE3:def 1;
lfp f is_a_fixpoint_of f by Th44;
then A2: lfp (A, g) c= lf by Th10;
reconsider lg = lfp(A, g) as Element of BooleLatt A by A1;
lg is_a_fixpoint_of f by Th6;
then lfp f [= lg by Th46;
then lf c= lg by LATTICE3:2;
hence lfp (A, g) = lfp f by A2,XBOOLE_0:def 10;
end;
theorem
ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f
proof
A1: 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 Th49;
take g;
reconsider gf = gfp f as Subset of A by LATTICE3:def 1;
gfp f is_a_fixpoint_of f by Th45;
then A2: gf c= gfp (A, g) by Th10;
reconsider gg = gfp(A, g) as Element of BooleLatt A by A1;
gg is_a_fixpoint_of f by Th7;
then gg [= gfp f by Th46;
then gg c= gf by LATTICE3:2;
hence gfp (A, g) = gfp f by A2,XBOOLE_0:def 10;
end;