:: Complete Lattices
:: by Grzegorz Bancerek
::
:: Received May 13, 1992
:: Copyright (c) 1992-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 LATTICES, STRUCT_0, ZFMISC_1, SUBSET_1, FUNCT_1, XBOOLE_0,
BINOP_1, EQREL_1, PBOOLE, TARSKI, FILTER_1, ORDERS_1, RELAT_1, RELAT_2,
ORDERS_2, XXREAL_0, REWRITE1, FILTER_0, XBOOLEAN, SETFAM_1, LATTICE3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0,
FUNCT_1, FUNCT_2, BINOP_1, LATTICES, FILTER_0, LATTICE2, FILTER_1,
RELAT_1, RELAT_2, RELSET_1, ORDERS_1, ORDERS_2;
constructors BINOP_1, DOMAIN_1, ORDERS_2, LATTICE2, FILTER_1, RELSET_1,
FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, ORDERS_2,
LATTICE2, RELAT_2;
requirements SUBSET, BOOLE;
definitions XBOOLE_0, TARSKI, LATTICES, RELAT_1, RELAT_2, ORDERS_2, STRUCT_0;
equalities LATTICES;
expansions XBOOLE_0, TARSKI, LATTICES, RELAT_2, ORDERS_2;
theorems TARSKI, ENUMSET1, ZFMISC_1, FUNCT_1, FUNCT_2, BINOP_1, LATTICES,
FILTER_0, FILTER_1, LATTICE2, RELAT_1, ORDERS_2, XBOOLE_0, XBOOLE_1,
RELAT_2, PARTFUN1, ORDERS_1, XTUPLE_0;
schemes FRAENKEL, BINOP_1, RELSET_1;
begin :: Boolean Lattice of Subsets
deffunc carr(LattStr) = the carrier of $1;
deffunc join(LattStr) = the L_join of $1;
deffunc met(LattStr) = the L_meet of $1;
definition
let X be set;
func BooleLatt X -> strict LattStr means
:Def1:
the carrier of it = bool X & for Y,Z being Subset of X holds
(the L_join of it).(Y,Z) = Y \/ Z & (the L_meet of it).(Y,Z) = Y /\ Z;
existence
proof
deffunc U(Subset of X,Subset of X) = $1 \/ $2;
consider j being BinOp of bool X such that
A1: for x,y being Subset of X holds j.(x,y) = U(x,y) from BINOP_1:sch 4;
deffunc U(Subset of X,Subset of X) = $1 /\ $2;
consider m being BinOp of bool X such that
A2: for x,y being Subset of X holds m.(x,y) = U(x,y) from BINOP_1:sch 4;
take LattStr(#bool X, j, m#);
thus thesis by A1,A2;
end;
uniqueness
proof
let L1, L2 be strict LattStr such that
A3: the carrier of L1 = bool X and
A4: for Y,Z being Subset of X holds join(L1).(Y,Z) = Y \/ Z & met(L1).(Y
,Z) = Y /\ Z and
A5: the carrier of L2 = bool X and
A6: for Y,Z being Subset of X holds join(L2).(Y,Z) = Y \/ Z & met(L2).(Y
,Z) = Y /\ Z;
reconsider j1 = join(L1), j2 = join(L2), m1 = met(L1), m2 = met(L2) as
BinOp of bool X by A3,A5;
now
let x,y be Subset of X;
thus j1.(x,y) = x \/ y by A4
.= j2.(x,y) by A6;
end;
then
A7: j1 = j2 by BINOP_1:2;
now
let x,y be Subset of X;
thus m1.(x,y) = x /\ y by A4
.= m2.(x,y) by A6;
end;
hence thesis by A3,A5,A7,BINOP_1:2;
end;
end;
reserve X for set,
x,y,z for Element of BooleLatt X,
s for set;
registration
let X be set;
cluster BooleLatt X -> non empty;
coherence
proof
the carrier of BooleLatt X = bool X by Def1;
hence the carrier of BooleLatt X is non empty;
end;
end;
registration
let X;
let x,y;
let x9,y9 be set;
identify x "\/" y with x9 \/ y9 when x = x9, y = y9;
compatibility
proof
reconsider x99 = x, y99 = y as Subset of X by Def1;
assume that
A1: x = x9 and
A2: y = y9;
thus x "\/" y = join(BooleLatt X).(x99,y99) .= x9 \/ y9 by A1,A2,Def1;
end;
identify x "/\" y with x9 /\ y9 when x = x9, y = y9;
compatibility
proof
reconsider x99 = x, y99 = y as Subset of X by Def1;
assume that
A3: x = x9 and
A4: y = y9;
thus x "/\" y = met(BooleLatt X).(x99,y99) .= x9 /\ y9 by A3,A4,Def1;
end;
end;
theorem Th1:
x "\/" y = x \/ y & x "/\" y = x /\ y;
theorem Th2:
x [= y iff x c= y by XBOOLE_1:7,XBOOLE_1:12;
registration
let X;
cluster BooleLatt X -> Lattice-like;
coherence
proof
A1: x"\/"(y"\/"z) = (x"\/"y)"\/"z by XBOOLE_1:4;
A2: (x"/\"y)"\/"y = y by XBOOLE_1:22;
A3: x"/\"(y"/\"z) = (x"/\"y)"/\"z by XBOOLE_1:16;
x"/\"(x"\/"y) = x by XBOOLE_1:21;
then BooleLatt X is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by A1,A2,A3;
hence thesis;
end;
end;
reserve y for Element of BooleLatt X;
theorem Th3:
BooleLatt X is lower-bounded & Bottom BooleLatt X = {}
proof {} c= X;
then reconsider x = {} as Element of BooleLatt X by Def1;
A1: x"/\"y = x;
A2: y"/\"x = x;
thus BooleLatt X is lower-bounded
proof
take x;
thus thesis;
end;
hence thesis by A1,A2,LATTICES:def 16;
end;
theorem Th4:
BooleLatt X is upper-bounded & Top BooleLatt X = X
proof
A1: bool X = carr(BooleLatt X) by Def1;
then reconsider x = X as Element of BooleLatt X by ZFMISC_1:def 1;
A2: x"\/"y = x by A1,XBOOLE_1:12;
A3: y"\/"x = x by A1,XBOOLE_1:12;
thus BooleLatt X is upper-bounded
proof
take x;
thus thesis by A1,XBOOLE_1:12;
end;
hence thesis by A2,A3,LATTICES:def 17;
end;
registration
let X;
cluster BooleLatt X -> Boolean;
coherence
proof
set B = BooleLatt X;
A1: B is 0_Lattice by Th3;
B is 1_Lattice by Th4;
then reconsider B as 01_Lattice by A1;
A2: B is complemented
proof
let x be Element of B;
A3: carr(B) = bool X by Def1;
reconsider y = X \ x as Element of B by Def1;
take y;
thus y"\/"x = y \/ x by Th1
.= X \/ x by XBOOLE_1:39
.= X by A3,XBOOLE_1:12
.= Top B by Th4;
hence x"\/"y = Top B;
A4: y misses x by XBOOLE_1:79;
thus y"/\"x = y /\ x by Th1
.= {} by A4
.= Bottom B by Th3;
hence thesis;
end;
B is distributive
proof
let x,y,z be Element of B;
thus x"/\"(y"\/"z) = x /\ (y"\/"z) by Th1
.= x /\ (y \/ z) by Th1
.= x/\y \/ x/\z by XBOOLE_1:23
.= (x"/\"y)\/(x/\z) by Th1
.= (x"/\"y)\/(x"/\"z) by Th1
.= (x"/\"y)"\/"(x"/\"z) by Th1;
end;
hence thesis by A2;
end;
end;
theorem
for x being Element of BooleLatt X holds x` = X \ x
proof
set B = BooleLatt X;
let x be Element of B;
A1: x`"/\"x = Bottom B by LATTICES:20;
A2: x"\/"x` = Top B by LATTICES:21;
A3: Bottom B = {} by Th3;
A4: Top B = X by Th4;
A5: x` misses x by A1,A3;
A6: X \ x = (x \ x) \/ (x` \ x) by A2,A4,XBOOLE_1:42;
x \ x = {} by XBOOLE_1:37;
hence thesis by A5,A6,XBOOLE_1:83;
end;
begin :: Correspondence Between Lattices and Posets
definition
let L be Lattice;
redefine func LattRel L -> Order of the carrier of L; :: redefines LattRel (FILTER_1, definition)
coherence
proof
A1: LattRel L = { [p,q] where p is Element of L, q is Element of L: p [= q }
by FILTER_1:def 8;
LattRel L c= [:carr(L),carr(L):]
proof
let x,y be object;
assume [x,y] in LattRel L;
then ex p,q being Element of L st [x,y] = [p,q] & p [= q by A1;
hence thesis by ZFMISC_1:87;
end;
then reconsider R = LattRel L as Relation of carr(L);
A2: R is_reflexive_in carr(L)
by FILTER_1:31;
A3: R is_antisymmetric_in carr(L)
proof
let x,y be object;
assume that
A4: x in carr(L) and
A5: y in carr(L);
reconsider x9 = x, y9 = y as Element of L by A4,A5;
assume that
A6: [x,y] in R and
A7: [y,x] in R;
A8: x9 [= y9 by A6,FILTER_1:31;
y9 [= x9 by A7,FILTER_1:31;
hence thesis by A8,LATTICES:8;
end;
A9: R is_transitive_in carr(L)
proof
let x,y,z be object;
assume that
A10: x in carr(L) and
A11: y in carr(L) and
A12: z in carr(L);
reconsider x9 = x, y9 = y, z9 = z as Element of L by A10,A11,A12;
assume that
A13: [x,y] in R and
A14: [y,z] in R;
A15: x9 [= y9 by A13,FILTER_1:31;
y9 [= z9 by A14,FILTER_1:31;
then x9 [= z9 by A15,LATTICES:7;
hence thesis by FILTER_1:31;
end;
A16: dom R = carr(L) by A2,ORDERS_1:13;
field R = carr(L) by A2,ORDERS_1:13;
hence thesis by A2,A3,A9,A16,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 16;
end;
end;
definition
let L be Lattice;
func LattPOSet L -> strict Poset equals
RelStr(#the carrier of L, LattRel L#);
correctness;
end;
registration
let L be Lattice;
cluster LattPOSet L -> non empty;
coherence;
end;
theorem Th6:
for L1,L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds
the LattStr of L1 = the LattStr of L2
proof
let L1,L2 be Lattice such that
A1: LattPOSet L1 = LattPOSet L2;
reconsider j = join(L2), m = met(L2) as BinOp of carr(L1) by A1;
now
let a,b be Element of L1;
reconsider x = a, y = b, xy = a"\/" b as Element of L2 by A1;
reconsider ab = x"\/"y as Element of L1 by A1;
A2: a [= a"\/"b by LATTICES:5;
A3: b [= b"\/"a by LATTICES:5;
A4: x [= x"\/"y by LATTICES:5;
A5: y [= y"\/"x by LATTICES:5;
A6: [x,xy] in LattRel L2 by A1,A2,FILTER_1:31;
A7: [y,xy] in LattRel L2 by A1,A3,FILTER_1:31;
A8: [a,ab] in LattRel L1 by A1,A4,FILTER_1:31;
A9: [b,ab] in LattRel L1 by A1,A5,FILTER_1:31;
A10: a [= ab by A8,FILTER_1:31;
A11: b [= ab by A9,FILTER_1:31;
A12: x [= xy by A6,FILTER_1:31;
A13: y [= xy by A7,FILTER_1:31;
A14: a"\/"b [= ab by A10,A11,FILTER_0:6;
x"\/"y [= xy by A12,A13,FILTER_0:6;
then [ab,a"\/"b] in LattRel L1 by A1,FILTER_1:31;
then ab [= a"\/"b by FILTER_1:31;
hence join(L1).(a,b) = j.(a,b) by A14,LATTICES:8;
end;
then
A15: join(L1) = j by BINOP_1:2;
now
let a,b be Element of L1;
reconsider x = a, y = b, xy = a"/\" b as Element of L2 by A1;
reconsider ab = x"/\"y as Element of L1 by A1;
A16: a"/\"b [= a by LATTICES:6;
A17: b"/\"a [= b by LATTICES:6;
A18: x"/\"y [= x by LATTICES:6;
A19: y"/\"x [= y by LATTICES:6;
A20: [xy,x] in LattRel L2 by A1,A16,FILTER_1:31;
A21: [xy,y] in LattRel L2 by A1,A17,FILTER_1:31;
A22: [ab,a] in LattRel L1 by A1,A18,FILTER_1:31;
A23: [ab,b] in LattRel L1 by A1,A19,FILTER_1:31;
A24: ab [= a by A22,FILTER_1:31;
A25: ab [= b by A23,FILTER_1:31;
A26: xy [= x by A20,FILTER_1:31;
A27: xy [= y by A21,FILTER_1:31;
A28: ab [= a"/\"b by A24,A25,FILTER_0:7;
xy [= x"/\"y by A26,A27,FILTER_0:7;
then [a"/\"b,ab] in LattRel L1 by A1,FILTER_1:31;
then a"/\"b [= ab by FILTER_1:31;
hence met(L1).(a,b) = m.(a,b) by A28,LATTICES:8;
end;
hence thesis by A1,A15,BINOP_1:2;
end;
definition
let L be Lattice, p be Element of L;
func p% -> Element of LattPOSet L equals
p;
correctness;
end;
definition
let L be Lattice, p be Element of LattPOSet L;
func %p -> Element of L equals
p;
correctness;
end;
reserve L for Lattice,
p,q for Element of L;
theorem Th7:
p [= q iff p% <= q%
by FILTER_1:31;
definition
let X be set, O be Order of X;
redefine func O~ -> Order of X; :: redefines ~ (RELAT_1, definition)
coherence
proof
A1: dom O = dom(O~) by RELAT_2:12;
dom O = X by PARTFUN1:def 2;
hence thesis by A1,PARTFUN1:def 2;
end;
end;
definition
let A be RelStr;
func A~ -> strict RelStr equals
RelStr(#the carrier of A, (the InternalRel of A)~#);
correctness;
end;
registration
let A be Poset;
cluster A~ -> reflexive transitive antisymmetric;
coherence
proof A~ = RelStr(#the carrier of A, (the InternalRel of A)~#);
hence thesis;
end;
end;
registration
let A be non empty RelStr;
cluster A~ -> non empty;
coherence;
end;
reserve A for RelStr,
a,b,c for Element of A;
theorem
A~~ = the RelStr of A;
definition
let A be RelStr, a be Element of A;
func a~ -> Element of A~ equals
a;
correctness;
end;
definition
let A be RelStr, a be Element of A~;
func ~a -> Element of A equals
a;
correctness;
end;
theorem Th9:
a <= b iff b~ <= a~
by RELAT_1:def 7;
definition
let A be RelStr, X be set, a be Element of A;
pred a is_<=_than X means
for b being Element of A st b in X holds a <= b;
pred X is_<=_than a means
for b being Element of A st b in X holds b <= a;
end;
notation
let A be RelStr, X be set, a be Element of A;
synonym X is_>=_than a for a is_<=_than X; synonym a is_>=_than X for
X is_<=_than a;
end;
definition
let IT be RelStr;
attr IT is with_suprema means
: Def10:
for x,y being Element of IT ex z being Element of IT st x <= z & y <= z &
for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9;
attr IT is with_infima means
: Def11:
for x,y being Element of IT ex z being Element of IT st z <= x & z <= y &
for z9 being Element of IT st z9 <= x & z9 <= y holds z9 <= z;
end;
registration
cluster with_suprema -> non empty for RelStr;
coherence
proof
let A be RelStr such that
A1: for x,y being Element of A ex z being Element of A st x <= z & y <= z &
for z9 being Element of A st x <= z9 & y <= z9 holds z <= z9;
set x = the Element of A;
consider z being Element of A such that
A2: x <= z and x <= z and
for z9 being Element of A st x <= z9 & x <= z9 holds z <= z9 by A1;
[x,z] in the InternalRel of A by A2;
hence thesis;
end;
cluster with_infima -> non empty for RelStr;
coherence
proof
let A be RelStr such that
A3: for x,y being Element of A ex z being Element of A st x >= z & y >= z &
for z9 being Element of A st x >= z9 & y >= z9 holds z >= z9;
set x = the Element of A;
consider z being Element of A such that
A4: x >= z and x >= z and
for z9 being Element of A st x >= z9 & x >= z9 holds z >= z9 by A3;
[z,x] in the InternalRel of A by A4;
hence thesis;
end;
end;
theorem
A is with_suprema iff A~ is with_infima
proof
thus A is with_suprema implies A~ is with_infima
proof
assume
A1: for a,b ex c st a <= c & b <= c &
for c9 being Element of A st a <= c9 & b <= c9 holds c <= c9;
let x,y be Element of A~;
consider c such that
A2: ~x <= c and
A3: ~y <= c and
A4: for c9 being Element of A st ~x <= c9 & ~y <= c9 holds c <= c9 by A1;
take z = c~;
A5: (~x)~ = ~x;
A6: (~y)~ = ~y;
hence z <= x & z <= y by A2,A3,A5,Th9;
let z9 be Element of A~;
A7: (~z9)~ = ~z9;
assume that
A8: z9 <= x and
A9: z9 <= y;
A10: ~x <= ~z9 by A5,A7,A8,Th9;
~y <= ~z9 by A6,A7,A9,Th9;
then c <= ~z9 by A4,A10;
hence thesis by A7,Th9;
end;
assume
A11: for x,y being Element of A~ ex z being Element of A~ st z <= x & z <= y &
for z9 being Element of A~ st z9 <= x & z9 <= y holds z9 <= z;
let a,b;
consider z being Element of A~ such that
A12: z <= a~ and
A13: z <= b~ and
A14: for z9 being Element of A~ st z9 <= a~ & z9 <= b~ holds z9 <= z by A11;
take c = ~z;
A15: (~z)~ = ~z;
hence a <= c & b <= c by A12,A13,Th9;
let c9 be Element of A;
assume that
A16: a <= c9 and
A17: b <= c9;
A18: c9~ <= a~ by A16,Th9;
c9~ <= b~ by A17,Th9;
then c9~ <= z by A14,A18;
hence thesis by A15,Th9;
end;
theorem
for L being Lattice holds LattPOSet L is with_suprema with_infima
proof
let L;
thus LattPOSet L is with_suprema
proof
let x,y be Element of LattPOSet L;
take z = (%x"\/"%y)%;
A1: %x [= %x"\/"%y by LATTICES:5;
A2: %y [= %y"\/"%x by LATTICES:5;
A3: (%x)% = %x;
A4: (%y)% = %y;
hence x <= z & y <= z by A1,A2,A3,Th7;
let z9 be Element of LattPOSet L;
A5: (%z9)% = %z9;
assume that
A6: x <= z9 and
A7: y <= z9;
A8: %x [= %z9 by A3,A5,A6,Th7;
%y [= %z9 by A4,A5,A7,Th7;
then %x"\/"%y [= %z9 by A8,FILTER_0:6;
hence thesis by A5,Th7;
end;
let x,y be Element of LattPOSet L;
take z = (%x"/\"%y)%;
A9: %x"/\"%y [= %x by LATTICES:6;
A10: %y"/\"%x [= %y by LATTICES:6;
A11: (%x)% = %x;
A12: (%y)% = %y;
hence z <= x & z <= y by A9,A10,A11,Th7;
let z9 be Element of LattPOSet L;
A13: (%z9)% = %z9;
assume that
A14: z9 <= x and
A15: z9 <= y;
A16: %z9 [= %x by A11,A13,A14,Th7;
%z9 [= %y by A12,A13,A15,Th7;
then %z9 [= %x"/\"%y by A16,FILTER_0:7;
hence thesis by A13,Th7;
end;
definition
let IT be RelStr;
attr IT is complete means
:
Def12: for X being set ex a being Element of IT st X is_<=_than a &
for b being Element of IT st X is_<=_than b holds a <= b;
end;
registration
cluster strict complete non empty for Poset;
existence
proof set s = the set;
set D = {s};
set R = the Order of D;
take A = RelStr(#D, R#);
thus A is strict;
hereby
let X be set;
reconsider s as Element of A by TARSKI:def 1;
take s;
thus X is_<=_than s
proof
let a be Element of A such that a in X;
thus a <= s by TARSKI:def 1;
end;
let b be Element of A such that X is_<=_than b;
thus
s <= b by TARSKI:def 1;
end;
thus thesis;
end;
end;
reserve A for non empty RelStr,
a,b,c,c9 for Element of A;
theorem Th12:
A is complete implies A is with_suprema with_infima
proof
assume
A1: for X being set ex a st X is_<=_than a &
for b st X is_<=_than b holds a <= b;
thus A is with_suprema
proof
let a,b;
consider c such that
A2: {a,b} is_<=_than c and
A3: for c9 st {a,b} is_<=_than c9 holds c <= c9 by A1;
take c;
A4: a in {a,b} by TARSKI:def 2;
b in {a,b} by TARSKI:def 2;
hence a <= c & b <= c by A2,A4;
let c9 such that
A5: a <= c9 and
A6: b <= c9;
{a,b} is_<=_than c9
by A5,A6,TARSKI:def 2;
hence thesis by A3;
end;
let a,b;
set X = {c: c <= a & c <= b};
consider c such that
A7: X is_<=_than c and
A8: for c9 st X is_<=_than c9 holds c <= c9 by A1;
take c;
X is_<=_than a
proof
let c;
assume c in X;
then ex c9 st c = c9 & c9 <= a & c9 <= b;
hence thesis;
end;
hence c <= a by A8;
X is_<=_than b
proof
let c;
assume c in X;
then ex c9 st c = c9 & c9 <= a & c9 <= b;
hence thesis;
end;
hence c <= b by A8;
let c9;
assume that
A9: c9 <= a and
A10: c9 <= b;
c9 in X by A9,A10;
hence thesis by A7;
end;
registration
cluster complete with_suprema with_infima strict non empty for Poset;
existence
proof set A = the complete strict non empty Poset;
take A;
thus thesis by Th12;
end;
end;
definition
let A be RelStr such that
A1: A is antisymmetric;
let a,b be Element of A such that
A2: ex x being Element of A st a <= x & b <= x &
for c being Element of A st a <= c & b <= c holds x <= c;
func a"\/"b -> Element of A means
:Def13:
a <= it & b <= it &
for c being Element of A st a <= c & b <= c holds it <= c;
existence by A2;
uniqueness
proof
let c1,c2 be Element of A such that
A3: a <= c1 and
A4: b <= c1 and
A5: for c being Element of A st a <= c & b <= c holds c1 <= c and
A6: a <= c2 and
A7: b <= c2 and
A8: for c being Element of A st a <= c & b <= c holds c2 <= c;
A9: c1 <= c2 by A5,A6,A7;
c2 <= c1 by A3,A4,A8;
hence thesis by A1,A9,ORDERS_2:2;
end;
end;
Lm1: now
let A be non empty antisymmetric with_suprema RelStr;
let a,b be Element of A;
ex x being Element of A st a <= x & b <= x &
for c being Element of A st a <= c & b <= c holds x <= c by Def10;
hence for c being Element of A holds c = a"\/"b iff
a <= c & b <= c & for d being Element of A st a <= d & b <= d holds c <= d
by Def13;
end;
definition
let A be RelStr such that
A1: A is antisymmetric;
let a,b be Element of A such that
A2: ex x being Element of A st a >= x & b >= x &
for c being Element of A st a >= c & b >= c holds x >= c;
func a"/\"b -> Element of A means
:Def14:
it <= a & it <= b &
for c being Element of A st c <= a & c <= b holds c <= it;
existence by A2;
uniqueness
proof
let c1,c2 be Element of A such that
A3: c1 <= a and
A4: c1 <= b and
A5: for c being Element of A st c <= a & c <= b holds c <= c1 and
A6: c2 <= a and
A7: c2 <= b and
A8: for c being Element of A st c <= a & c <= b holds c <= c2;
A9: c1 <= c2 by A3,A4,A8;
c2 <= c1 by A5,A6,A7;
hence thesis by A1,A9,ORDERS_2:2;
end;
end;
Lm2: now
let A be non empty antisymmetric with_infima RelStr;
let a,b be Element of A;
ex x being Element of A st a >= x & b >= x &
for c being Element of A st a >= c & b >= c holds x >= c by Def11;
hence for c being Element of A holds c = a"/\"b iff
a >= c & b >= c & for d being Element of A st a >= d & b >= d holds c >= d
by Def14;
end;
reserve V for with_suprema antisymmetric RelStr,
u1,u2,u3,u4 for Element of V;
reserve N for with_infima antisymmetric RelStr,
n1,n2,n3,n4 for Element of N;
reserve K for with_suprema with_infima reflexive antisymmetric RelStr,
k1,k2,k3 for Element of K;
theorem Th13:
u1 "\/" u2 = u2 "\/" u1
proof
A1: u1 <= u1"\/"u2 by Lm1;
A2: u2 <= u1"\/"u2 by Lm1;
for u3 st u2 <= u3 & u1 <= u3 holds u1"\/"u2 <= u3 by Lm1;
hence thesis by A1,A2,Def13;
end;
theorem Th14:
V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
proof
assume
A1: V is transitive;
A2: u1 <= u1"\/"u2 by Lm1;
A3: u2 <= u1"\/"u2 by Lm1;
A4: u2 <= u2"\/"u3 by Lm1;
A5: u3 <= u2"\/"u3 by Lm1;
A6: u1"\/"u2 <= (u1"\/"u2)"\/"u3 by Lm1;
A7: u3 <= (u1"\/"u2)"\/"u3 by Lm1;
A8: u1 <= (u1"\/"u2)"\/"u3 by A1,A2,A6,ORDERS_2:3;
u2 <= (u1"\/"u2)"\/"u3 by A1,A3,A6,ORDERS_2:3;
then
A9: u2"\/"u3 <= (u1"\/"u2)"\/"u3 by A7,Lm1;
now
let u4;
assume that
A10: u1 <= u4 and
A11: u2"\/"u3 <= u4;
A12: u2 <= u4 by A1,A4,A11,ORDERS_2:3;
A13: u3 <= u4 by A1,A5,A11,ORDERS_2:3;
u1"\/"u2 <= u4 by A10,A12,Lm1;
hence (u1"\/"u2)"\/"u3 <= u4 by A13,Lm1;
end;
hence thesis by A8,A9,Def13;
end;
theorem Th15:
n1 "/\" n2 = n2 "/\" n1
proof
A1: n1"/\"n2 <= n1 by Lm2;
A2: n1"/\"n2 <= n2 by Lm2;
for n3 st n3 <= n2 & n3 <= n1 holds n3 <= n1"/\"n2 by Lm2;
hence thesis by A1,A2,Def14;
end;
theorem Th16:
N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
proof
assume
A1: N is transitive;
A2: n1"/\"n2 <= n1 by Lm2;
A3: n1"/\"n2 <= n2 by Lm2;
A4: n2"/\"n3 <= n2 by Lm2;
A5: n2"/\"n3 <= n3 by Lm2;
A6: (n1"/\"n2)"/\"n3 <= n1"/\"n2 by Lm2;
A7: (n1"/\"n2)"/\"n3 <= n3 by Lm2;
A8: (n1"/\"n2)"/\"n3 <= n1 by A1,A2,A6,ORDERS_2:3;
(n1"/\"n2)"/\"n3 <= n2 by A1,A3,A6,ORDERS_2:3;
then
A9: (n1"/\"n2)"/\"n3 <= n2"/\"n3 by A7,Lm2;
now
let n4;
assume that
A10: n4 <= n1 and
A11: n4 <= n2"/\"n3;
A12: n4 <= n2 by A1,A4,A11,ORDERS_2:3;
A13: n4 <= n3 by A1,A5,A11,ORDERS_2:3;
n4 <= n1"/\"n2 by A10,A12,Lm2;
hence n4 <= (n1"/\"n2)"/\"n3 by A13,Lm2;
end;
hence thesis by A8,A9,Def14;
end;
definition
let L be with_infima antisymmetric RelStr, x, y be Element of L;
redefine func x "/\" y; :: redefines "/\" (LATTICE3, definition)
commutativity by Th15;
end;
definition
let L be with_suprema antisymmetric RelStr, x, y be Element of L;
redefine func x "\/" y; :: redefines "\/" (LATTICE3, definition)
commutativity by Th13;
end;
theorem Th17:
(k1 "/\" k2) "\/" k2 = k2
proof
A1: k1"/\"k2 <= k2 by Lm2;
A2: k2 <= k2;
for k3 st k1"/\" k2 <= k3 & k2 <= k3 holds k2 <= k3;
hence thesis by A1,A2,Def13;
end;
theorem Th18:
k1 "/\" (k1 "\/" k2) = k1
proof
A1: k1 <= k1;
A2: k1 <= k1"\/"k2 by Lm1;
for k3 st k3 <= k1 & k3 <= k1"\/" k2 holds k3 <= k1;
hence thesis by A1,A2,Def14;
end;
theorem Th19:
for A being with_suprema with_infima Poset
ex L being strict Lattice st the RelStr of A = LattPOSet L
proof
let A be with_suprema with_infima Poset;
defpred X[Element of A,Element of A,set] means
for x9,y9 being Element of A st x9 = $1 & y9 = $2 holds $3 = x9"\/"y9;
A1: for x,y being Element of A ex u being Element of A st X[x,y,u]
proof
let x,y be Element of A;
reconsider x9 = x, y9 = y as Element of A;
take x9"\/"y9;
thus thesis;
end;
consider j being BinOp of the carrier of A such that
A2: for x,y being Element of A holds X[x,y,j.(x,y)] from BINOP_1:sch 3(A1);
defpred X[Element of A,Element of A,set] means
for x9,y9 being Element of A st x9 = $1 & y9 = $2 holds $3 = x9"/\"y9;
A3: for x,y being Element of A ex u being Element of A st X[x,y,u]
proof
let x,y be Element of A;
reconsider x9 = x, y9 = y as Element of A;
take x9"/\"y9;
thus thesis;
end;
consider m being BinOp of the carrier of A such that
A4: for x,y being Element of A holds X[x,y,m.(x,y)] from BINOP_1:sch 3(A3);
set L = LattStr(#the carrier of A, j, m#);
A5: now
let a,b be Element of L;
reconsider x = a, y = b as Element of A;
j.(x,y) = x "\/"y by A2;
hence a"\/"b = b"\/"a by A2;
end;
A6: now
let a,b,c be Element of L;
reconsider x = a, y = b, z = c as Element of A;
thus a"\/"(b"\/"c) = j.(x,y"\/"z) by A2
.= x"\/"(y"\/"z) by A2
.= x"\/"y"\/"z by Th14
.= j.(x"\/"y,z) by A2
.= (a"\/"b)"\/"c by A2;
end;
A7: now
let a,b be Element of L;
reconsider x = a, y = b as Element of A;
thus (a"/\"b)"\/"b = j.(x"/\"y,y) by A4
.= (x"/\"y)"\/"y by A2
.= b by Th17;
end;
A8: now
let a,b be Element of L;
reconsider x = a, y = b as Element of A;
m.(x,y) = x "/\"y by A4;
hence a"/\"b = b"/\"a by A4;
end;
A9: now
let a,b,c be Element of L;
reconsider x = a, y = b, z = c as Element of A;
thus a"/\"(b"/\"c) = m.(x,y"/\"z) by A4
.= x"/\"(y"/\"z) by A4
.= x"/\"y"/\"z by Th16
.= m.(x"/\"y,z) by A4
.= (a"/\"b)"/\"c by A4;
end;
now
let a,b be Element of L;
reconsider x = a, y = b as Element of A;
thus a"/\"(a"\/"b) = m.(x,x"\/"y) by A2
.= x"/\"(x"\/"y) by A4
.= a by Th18;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by A5,A6,A7,A8,A9;
then reconsider L as strict Lattice;
take L;
A10: LattRel L = {[p,q] where p is Element of L, q is Element of L: p [= q}
by FILTER_1:def 8;
LattRel L = the InternalRel of A
proof
let x,y be object;
thus [x,y] in LattRel L implies [x,y] in the InternalRel of A
proof
assume [x,y] in LattRel L;
then consider p,q being Element of L such that
A11: [x,y] = [p,q] and
A12: p [= q by A10;
reconsider p9 = p, q9 = q as Element of A;
p9"\/"q9 = p"\/"q by A2
.= q by A12;
then p9 <= q9 by Lm1;
hence thesis by A11;
end;
assume
A13: [x,y] in the InternalRel of A;
then consider x1,x2 being object such that
A14: x1 in the carrier of A and
A15: x2 in the carrier of A and
A16: [x,y] = [x1,x2] by ZFMISC_1:84;
reconsider x1, x2 as Element of A by A14,A15;
reconsider y1 = x1, y2 = x2 as Element of L;
A17: x1 <= x2 by A13,A16;
x2 <= x2;
then
A18: x1"\/"x2 <= x2 by A17,Lm1;
x2 <= x1"\/"x2 by Lm1;
then x2 = x1"\/"x2 by A18,ORDERS_2:2
.= y1"\/"y2 by A2;
then y1 [= y2;
hence thesis by A10,A16;
end;
hence thesis;
end;
definition
let A be RelStr such that
A1: A is with_suprema with_infima Poset;
func latt A -> strict Lattice means
: Def15:
the RelStr of A = LattPOSet it;
existence by A1,Th19;
uniqueness by Th6;
end;
theorem
(LattRel L)~ = LattRel (L.:) & (LattPOSet L)~ = LattPOSet (L.:)
proof
A1: LattRel L = {[p,q]: p [= q} by FILTER_1:def 8;
A2: LattRel (L.:) = {[p9,q9] where p9 is Element of L.:, q9 is Element of L
.: : p9 [= q9} by FILTER_1:def 8;
A3: L.: = LattStr(#carr(L), met(L), join(L)#) by LATTICE2:def 2;
thus (LattRel L)~ = LattRel (L.:)
proof
let x,y be object;
thus [x,y] in (LattRel L)~ implies [x,y] in LattRel (L.:)
proof
assume [x,y] in (LattRel L)~;
then [y,x] in LattRel L by RELAT_1:def 7;
then consider p,q such that
A4: [y,x] = [p,q] and
A5: p [= q by A1;
reconsider p9 = p, q9 = q as Element of L.: by A3;
A6: x = q by A4,XTUPLE_0:1;
A7: y = p by A4,XTUPLE_0:1;
q9 [= p9 by A5,LATTICE2:38;
hence thesis by A2,A6,A7;
end;
assume [x,y] in LattRel (L.:);
then consider p9, q9 being Element of L.: such that
A8: [x,y] = [p9,q9] and
A9: p9 [= q9 by A2;
reconsider p = p9, q = q9 as Element of L by A3;
A10: x = p by A8,XTUPLE_0:1;
A11: y = q by A8,XTUPLE_0:1;
q [= p by A9,LATTICE2:39;
then [y,x] in LattRel L by A1,A10,A11;
hence thesis by RELAT_1:def 7;
end;
hence thesis by A3;
end;
begin :: Complete Lattice
definition
let L be non empty LattStr, p be Element of L, X be set;
pred p is_less_than X means
for q being Element of L st q in X holds p [= q;
pred X is_less_than p means
for q being Element of L st q in X holds q [= p;
end;
notation
let L be non empty LattStr, p be Element of L, X be set;
synonym X is_greater_than p for p is_less_than X;
synonym p is_greater_than X for X is_less_than p;
end;
theorem
for L being Lattice, p,q,r being Element of L holds
p is_less_than {q,r} iff p [= q"/\"r
proof
let L be Lattice, p,q,r be Element of L;
A1: q in {q,r} by TARSKI:def 2;
A2: r in {q,r} by TARSKI:def 2;
thus p is_less_than {q,r} implies p [= q"/\"r
proof
assume
A3: p is_less_than {q,r};
then
A4: p [= q by A1;
p [= r by A2,A3;
hence thesis by A4,FILTER_0:7;
end;
assume
A5: p [= q"/\"r;
let a be Element of L;
assume a in {q,r};
then
A6: a = q or a = r by TARSKI:def 2;
A7: q"/\"r [= q by LATTICES:6;
r"/\"q [= r by LATTICES:6;
hence thesis by A5,A6,A7,LATTICES:7;
end;
theorem
for L being Lattice, p,q,r being Element of L holds
p is_greater_than {q,r} iff q"\/"r [= p
proof
let L be Lattice, p,q,r be Element of L;
A1: q in {q,r} by TARSKI:def 2;
A2: r in {q,r} by TARSKI:def 2;
thus p is_greater_than {q,r} implies q"\/"r [= p
proof
assume
A3: p is_greater_than {q,r};
then
A4: q [= p by A1;
r [= p by A2,A3;
hence thesis by A4,FILTER_0:6;
end;
assume
A5: q"\/"r [= p;
let a be Element of L;
assume a in {q,r};
then
A6: a = q or a = r by TARSKI:def 2;
A7: q [= q"\/"r by LATTICES:5;
r [= r"\/"q by LATTICES:5;
hence thesis by A5,A6,A7,LATTICES:7;
end;
definition
let IT be non empty LattStr;
attr IT is complete means
:Def18:
for X being set ex p being Element of IT st X is_less_than p &
for r being Element of IT st X is_less_than r holds p [= r;
attr IT is \/-distributive means
for X for a,b,c being Element of IT st X is_less_than a &
(for d being Element of IT st X is_less_than d holds a [= d)
& {b"/\"a9 where a9 is Element of IT: a9 in X} is_less_than c &
for d being Element of IT st
{b"/\"a9 where a9 is Element of IT: a9 in X} is_less_than d holds c [= d
holds b"/\"a [= c;
attr IT is /\-distributive means
for X for a,b,c being Element of IT st X is_greater_than a &
(for d being Element of IT st X is_greater_than d holds d [= a)
& {b"\/"a9 where a9 is Element of IT: a9 in X} is_greater_than c &
for d being Element of IT st
{b"\/"a9 where a9 is Element of IT: a9 in X} is_greater_than d holds d [= c
holds c [= b"\/"a;
end;
theorem
for B being B_Lattice, a being Element of B holds
X is_less_than a iff {b` where b is Element of B: b in X} is_greater_than a`
proof
let B be B_Lattice, a be Element of B;
set Y = {b` where b is Element of B: b in X};
thus X is_less_than a implies Y is_greater_than a`
proof
assume
A1: for b being Element of B st b in X holds b [= a;
let b be Element of B;
assume b in Y;
then ex c being Element of B st ( b = c`)&( c in X);
hence thesis by A1,LATTICES:26;
end;
assume
A2: for b being Element of B st b in Y holds a` [= b;
let b be Element of B;
assume b in X;
then
A3: b` in Y;
A4: a`` = a;
b`` = b;
hence thesis by A2,A3,A4,LATTICES:26;
end;
theorem Th24:
for B being B_Lattice, a being Element of B holds
X is_greater_than a iff {b` where b is Element of B: b in X} is_less_than a`
proof
let B be B_Lattice, a be Element of B;
set Y = {b` where b is Element of B: b in X};
thus X is_greater_than a implies Y is_less_than a`
proof
assume
A1: for b being Element of B st b in X holds a [= b;
let b be Element of B;
assume b in Y;
then ex c being Element of B st ( b = c`)&( c in X);
hence thesis by A1,LATTICES:26;
end;
assume
A2: for b being Element of B st b in Y holds b [= a`;
let b be Element of B;
assume b in X;
then
A3: b` in Y;
A4: a`` = a;
b`` = b;
hence thesis by A2,A3,A4,LATTICES:26;
end;
theorem Th25:
BooleLatt X is complete
proof
set B = BooleLatt X;
let x be set;
set p = union (x /\ bool X);
A1: carr(B) = bool X by Def1;
reconsider p as Element of B by Def1;
take p;
thus x is_less_than p
proof
let q be Element of B;
assume q in x;
then q in x /\ bool X by A1,XBOOLE_0:def 4;
then q c= p by ZFMISC_1:74;
hence thesis by Th2;
end;
let r be Element of B such that
A2: for q being Element of B st q in x holds q [= r;
now
let z be set;
assume
A3: z in x /\ bool X;
then
A4: z in x by XBOOLE_0:def 4;
reconsider z9 = z as Element of B by A1,A3;
z9 [= r by A2,A4;
hence z c= r by Th2;
end;
then p c= r by ZFMISC_1:76;
hence thesis by Th2;
end;
registration
let X be set;
cluster BooleLatt X -> complete;
coherence by Th25;
end;
theorem Th26:
BooleLatt X is \/-distributive
proof
let x be set;
set B = BooleLatt X;
let a,b,c be Element of B such that
A1: x is_less_than a and
A2: for d being Element of B st x is_less_than d holds a [= d and
A3: {b"/\" a9 where a9 is Element of B: a9 in x} is_less_than c and
A4: for d being Element of B st
{b"/\"a9 where a9 is Element of B: a9 in x} is_less_than d holds c [= d;
set Y = {b"/\"a9 where a9 is Element of B: a9 in x};
A5: carr(B) = bool X by Def1;
A6: Y c= bool X
proof
let z be object;
assume z in Y;
then ex a9 being Element of B st z = b"/\"a9 & a9 in x;
hence thesis by A5;
end;
A7: (union Y) c= union bool X by A6,ZFMISC_1:77;
union bool X = X by ZFMISC_1:81;
then reconsider
p = union (x /\ bool X),q = union Y as Element of B by A7,Def1;
now
let y be set;
assume
A8: y in x /\ bool X;
then
A9: y in x by XBOOLE_0:def 4;
reconsider y9 = y as Element of B by A5,A8;
y9 [= a by A1,A9;
hence y c= a by Th2;
end;
then
A10: p c= a by ZFMISC_1:76;
A11: x is_less_than p
proof
let q be Element of B;
assume q in x;
then q in x /\ bool X by A5,XBOOLE_0:def 4;
then q c= p by ZFMISC_1:74;
hence q [= p by Th2;
end;
A12: p [= a by A10,Th2;
a [= p by A2,A11;
then
A13: a = p by A12;
now
let y be set;
assume
A14: y in Y;
then consider a9 being Element of B such that
A15: y = b"/\"a9 and a9 in x;
b"/\"a9 [= c by A3,A14,A15;
hence y c= c by A15,Th2;
end;
then
A16: q c= c by ZFMISC_1:76;
A17: Y is_less_than q
by ZFMISC_1:74,Th2;
A18: q [= c by A16,Th2;
c [= q by A4,A17;
then
A19: c = q by A18;
b /\ a c= c
proof
let z be object;
assume
A20: z in b /\ a;
then
A21: z in b by XBOOLE_0:def 4;
z in a by A20,XBOOLE_0:def 4;
then consider y being set such that
A22: z in y and
A23: y in x /\ bool X by A13,TARSKI:def 4;
A24: y in x by A23,XBOOLE_0:def 4;
reconsider y as Element of B by A5,A23;
A25: b"/\"y in Y by A24;
z in b /\ y by A21,A22,XBOOLE_0:def 4;
hence thesis by A19,A25,TARSKI:def 4;
end;
hence b"/\"a [= c by Th2;
end;
theorem Th27:
BooleLatt X is /\-distributive
proof
let x be set;
set B = BooleLatt X;
let a,b,c be Element of B such that
A1: x is_greater_than a and
A2: for d being Element of B st x is_greater_than d holds d [= a and
A3: {b"\/"a9 where a9 is Element of B: a9 in x} is_greater_than c and
A4: for d being Element of B st
{b"\/"a9 where a9 is Element of B: a9 in x} is_greater_than d holds d [= c;
set x9 = {e` where e is Element of B: e in x},
y = {b"\/"e where e is Element of B: e in x},
y9 = {e` where e is Element of B: e in y},
z = {b`"/\"e where e is Element of B: e in x9};
A5: z = y9
proof
thus z c= y9
proof
let s be object;
assume s in z;
then consider e being Element of B such that
A6: s = b`"/\"e and
A7: e in x9;
consider i being Element of B such that
A8: e = i` and
A9: i in x by A7;
A10: b"\/"i in y by A9;
(b"\/"i)` = s by A6,A8,LATTICES:24;
hence thesis by A10;
end;
let s be object;
assume s in y9;
then consider e being Element of B such that
A11: s = e` and
A12: e in y;
consider i being Element of B such that
A13: e = b"\/"i and
A14: i in x by A12;
A15: i` in x9 by A14;
s = b`"/\"i` by A11,A13,LATTICES:24;
hence thesis by A15;
end;
A16: c`` = c;
A17: x9 is_less_than a` by A1,Th24;
A18: for d being Element of B st x9 is_less_than d holds a` [= d
proof
let d be Element of B;
A19: d`` = d;
assume x9 is_less_than d;
then x is_greater_than d` by A19,Th24;
hence thesis by A2,A19,LATTICES:26;
end;
A20: z is_less_than c` by A3,A5,Th24;
A21: for d being Element of B st z is_less_than d holds c` [= d
proof
let d be Element of B;
A22: d`` = d;
assume z is_less_than d;
then y is_greater_than d` by A5,A22,Th24;
hence thesis by A4,A22,LATTICES:26;
end;
B is \/-distributive by Th26;
then
A23: b`"/\"a` [= c` by A17,A18,A20,A21;
(b`"/\"a`)` = b``"\/" a`` by LATTICES:23;
hence c [= b"\/"a by A16,A23,LATTICES:26;
end;
registration
cluster complete \/-distributive /\-distributive strict for Lattice;
existence
proof set X = the set;
BooleLatt X is complete \/-distributive /\-distributive by Th26,Th27;
hence thesis;
end;
end;
reserve p9,q9 for Element of LattPOSet L;
theorem Th28:
p is_less_than X iff p% is_<=_than X
proof
thus p is_less_than X implies p% is_<=_than X
proof
assume
A1: for q st q in X holds p [= q;
let p9;
A2: (%p9)% = %p9;
assume p9 in X;
then p [= %p9 by A1;
hence thesis by A2,Th7;
end;
assume
A3: for q9 st q9 in X holds p% <= q9;
let q;
assume q in X;
then p% <= q% by A3;
hence thesis by Th7;
end;
theorem
p9 is_<=_than X iff %p9 is_less_than X proof (%p9)% = %p9;
hence thesis by Th28;
end;
theorem Th30:
X is_less_than p iff X is_<=_than p%
proof
thus X is_less_than p implies X is_<=_than p%
proof
assume
A1: for q st q in X holds q [= p;
let p9;
A2: (%p9)% = %p9;
assume p9 in X;
then %p9 [= p by A1;
hence thesis by A2,Th7;
end;
assume
A3: for q9 st q9 in X holds q9 <= p%;
let q;
assume q in X;
then q% <= p% by A3;
hence thesis by Th7;
end;
theorem Th31:
X is_<=_than p9 iff X is_less_than %p9 proof (%p9)% = %p9;
hence thesis by Th30;
end;
registration
let A be complete non empty Poset;
cluster latt A -> complete;
coherence
proof A is with_suprema with_infima by Th12;
then
A1: the RelStr of A = LattPOSet latt A by Def15;
set B = LattPOSet latt A;
latt A is complete
proof
let X;
consider a being Element of A such that
A2: X is_<=_than a and
A3: for b being Element of A st X is_<=_than b holds a <= b by Def12;
reconsider a9 = a as Element of B by A1;
take p = %a9;
A4: p% = p;
thus X is_less_than p
proof
let q be Element of latt A;
reconsider b = q as Element of A by A1;
assume q in X;
then b <= a by A2;
then [b,a] in the InternalRel of A;
then q% <= a9 by A1;
hence q [= p by A4,Th7;
end;
let q be Element of latt A;
assume X is_less_than q;
then
A5: X is_<=_than q% by Th30;
reconsider b = q% as Element of A by A1;
X is_<=_than b
proof
let c be Element of A;
reconsider c9 = c as Element of B by A1;
assume c in X;
then c9 <= q% by A5;
then [c,b] in the InternalRel of the RelStr of A by A1;
hence c <= b;
end;
then a <= b by A3;
then [a,b] in the InternalRel of A;
then a9 <= q% by A1;
hence thesis by A4,Th7;
end;
hence thesis;
end;
end;
definition
let L be non empty LattStr such that
A1: L is complete Lattice;
let X be set;
func "\/"(X,L) -> Element of L means
: Def21:
X is_less_than it &
for r being Element of L st X is_less_than r holds it [= r;
existence by A1,Def18;
uniqueness
proof
let p1, p2 be Element of L such that
A2: X is_less_than p1 and
A3: for r being Element of L st X is_less_than r holds p1 [= r and
A4: X is_less_than p2 and
A5: for r being Element of L st X is_less_than r holds p2 [= r;
A6: p1 [= p2 by A3,A4;
p2 [= p1 by A2,A5;
hence thesis by A1,A6,LATTICES:8;
end;
end;
definition
let L be non empty LattStr, X be set;
func "/\"(X,L) -> Element of L equals
"\/"({p where p is Element of L: p is_less_than X},L);
correctness;
end;
notation
let L be non empty LattStr, X be Subset of L;
synonym "\/" X for "\/"(X,L); synonym "/\" X for "/\"(X,L);
end;
reserve C for complete Lattice,
a,a9,b,b9,c,d for Element of C,
X,Y for set;
theorem Th32:
"\/"({a"/\"b: b in X}, C) [= a"/\""\/"(X,C)
proof
set Y = {a"/\"b: b in X};
Y is_less_than a"/\""\/"(X,C)
proof
let c;
assume c in Y;
then consider b such that
A1: c = a"/\"b and
A2: b in X;
X is_less_than "\/"(X,C) by Def21;
then b [= "\/"(X,C) by A2;
hence thesis by A1,LATTICES:9;
end;
hence thesis by Def21;
end;
theorem Th33:
C is \/-distributive iff for X, a holds a"/\""\/"(X,C) [= "\/"({a"/\"
b: b in X}, C)
proof
thus C is \/-distributive implies for X, a holds
a"/\""\/"(X,C) [= "\/"({a"/\"b: b in X}, C)
proof
assume
A1: for X for a,b,c st X is_less_than a &
(for d st X is_less_than d holds a [= d) &
{b"/\"a9: a9 in X} is_less_than c &
for d st {b"/\"b9: b9 in X} is_less_than d holds c [= d holds b"/\"a [= c;
let X, a;
set Y = {a"/\"b: b in X};
A2: X is_less_than "\/"(X,C) by Def21;
A3: for d st X is_less_than d holds "\/"(X,C) [= d by Def21;
A4: Y is_less_than "\/"(Y,C) by Def21;
for d st Y is_less_than d holds "\/"(Y,C) [= d by Def21;
hence thesis by A1,A2,A3,A4;
end;
assume
A5: for X, a holds a"/\""\/"(X,C) [= "\/"({a"/\"b: b in X}, C);
let X;
let a,b,c;
assume
A6: X is_less_than a & (for d st X is_less_than d holds a [= d) &
{b"/\"a9: a9 in X} is_less_than c &
for d st {b"/\"b9: b9 in X} is_less_than d holds c [= d;
then
A7: a = "\/"(X,C) by Def21;
c = "\/"({b"/\"a9: a9 in X}, C) by A6,Def21;
hence b"/\"a [= c by A5,A7;
end;
theorem Th34:
a = "/\"(X,C) iff a is_less_than X & for b st b is_less_than X holds b [= a
proof
set Y = {b: b is_less_than X};
A1: a = "/\"(X,C) iff Y is_less_than a &
for c st Y is_less_than c holds a [= c by Def21;
thus a = "/\"(X,C) implies a is_less_than X &
for b st b is_less_than X holds b [= a
proof
assume
A2: a = "/\"(X,C);
then
A3: Y is_less_than a by Def21;
thus a is_less_than X
proof
let b such that
A4: b in X;
Y is_less_than b
proof
let c;
assume c in Y;
then ex d being Element of C st c = d & d is_less_than X;
hence thesis by A4;
end;
hence thesis by A2,Def21;
end;
let b;
assume b is_less_than X;
then b in Y;
hence thesis by A3;
end;
assume that
A5: a is_less_than X and
A6: for b st b is_less_than X holds b [= a;
A7: Y is_less_than a
proof
let b;
assume b in Y;
then ex c st b = c & c is_less_than X;
hence thesis by A6;
end;
a in Y by A5;
hence thesis by A1,A7;
end;
theorem Th35:
a"\/""/\"(X,C) [= "/\"({a"\/"b: b in X}, C)
proof
set Y = {a"\/"b: b in X};
Y is_greater_than a"\/""/\"(X,C)
proof
let c;
assume c in Y;
then consider b such that
A1: c = a"\/"b and
A2: b in X;
X is_greater_than "/\"(X,C) by Th34;
then "/\"(X,C) [= b by A2;
hence thesis by A1,FILTER_0:1;
end;
hence thesis by Th34;
end;
theorem Th36:
C is /\-distributive iff for X, a holds "/\"({a"\/"b: b in X}, C) [= a"\/""/\"
(X,C)
proof
thus C is /\-distributive implies for X, a holds
"/\"({a"\/"b: b in X}, C) [= a"\/""/\"(X,C)
proof
assume
A1: for X for a,b,c st X is_greater_than a &
(for d st X is_greater_than d holds d [= a) &
{b"\/"a9: a9 in X} is_greater_than c &
for d st {b"\/"b9: b9 in X} is_greater_than d holds d [= c
holds c [= b"\/"a;
let X, a;
set Y = {a"\/"b: b in X};
A2: X is_greater_than "/\"(X,C) by Th34;
A3: for d st X is_greater_than d holds d [= "/\"(X,C) by Th34;
A4: Y is_greater_than "/\"(Y,C) by Th34;
for d st Y is_greater_than d holds d [= "/\"(Y,C) by Th34;
hence thesis by A1,A2,A3,A4;
end;
assume
A5: for X, a holds "/\"({a"\/"b: b in X}, C) [= a"\/""/\"(X,C);
let X;
let a,b,c;
assume
A6: X is_greater_than a & (for d st X is_greater_than d holds d [= a) &
{b"\/"a9: a9 in X} is_greater_than c &
for d st {b"\/"b9: b9 in X} is_greater_than d holds d [= c;
then
A7: a = "/\"(X,C) by Th34;
c = "/\"({b"\/"a9: a9 in X}, C) by A6,Th34;
hence c [= b"\/"a by A5,A7;
end;
theorem
"\/"(X,C) = "/\"({a: a is_greater_than X}, C)
proof
set Y = {a: a is_greater_than X};
A1: "\/"(X,C) is_less_than Y
proof
let a;
assume a in Y;
then ex b st a = b & b is_greater_than X;
hence thesis by Def21;
end;
X is_less_than "\/"(X,C) by Def21;
then "\/"(X,C) in Y;
then for b st b is_less_than Y holds b [= "\/"(X,C);
hence thesis by A1,Th34;
end;
theorem Th38:
a in X implies a [= "\/"(X,C) & "/\"(X,C) [= a
proof
assume
A1: a in X;
X is_less_than "\/"(X,C) by Def21;
hence a [= "\/"(X,C) by A1;
{b: b is_less_than X} is_less_than a
proof
let c;
assume c in {b: b is_less_than X};
then ex b st c = b & b is_less_than X;
hence c [= a by A1;
end;
hence thesis by Def21;
end;
theorem Th39:
a is_less_than X implies a [= "/\"(X,C)
proof
assume a is_less_than X;
then a in {b: b is_less_than X};
hence thesis by Th38;
end;
theorem Th40:
a in X & X is_less_than a implies "\/"(X,C) = a
proof
assume that
A1: a in X and
A2: X is_less_than a;
A3: "\/"(X,C) [= a by A2,Def21;
a [= "\/"(X,C) by A1,Th38;
hence thesis by A3,LATTICES:8;
end;
theorem Th41:
a in X & a is_less_than X implies "/\"(X,C) = a
proof
assume that
A1: a in X and
A2: a is_less_than X;
A3: "/\"(X,C) [= a by A1,Th38;
a [= "/\"(X,C) by A2,Th39;
hence thesis by A3,LATTICES:8;
end;
theorem
"\/"{a} = a & "/\"{a} = a
proof
A1: a in {a} by TARSKI:def 1;
{a} is_less_than a
proof
let b;
assume b in {a};
hence b [= a by TARSKI:def 1;
end;
hence "\/"{a} = a by A1,Th40;
a is_less_than {a}
proof
let b;
assume b in {a};
hence a [= b by TARSKI:def 1;
end;
hence thesis by A1,Th41;
end;
theorem
a"\/"b = "\/"{a,b} & a"/\"b = "/\"{a,b}
proof
A1: {a,b} is_less_than a"\/"b
proof
let c;
assume
A2: c in {a,b};
A3: a [= a"\/"b by LATTICES:5;
b [= b"\/"a by LATTICES:5;
hence thesis by A2,A3,TARSKI:def 2;
end;
A4: a in {a,b} by TARSKI:def 2;
A5: b in {a,b} by TARSKI:def 2;
now
let c;
assume
A6: {a,b} is_less_than c;
then
A7: a [= c by A4;
b [= c by A5,A6;
hence a"\/"b [= c by A7,FILTER_0:6;
end;
hence a"\/"b = "\/"{a,b} by A1,Def21;
a"/\"b is_less_than {a,b}
proof
let c;
assume c in {a,b};
then c = a or c = b & b"/\"a = a"/\"b by TARSKI:def 2;
hence thesis by LATTICES:6;
end;
then
A8: a"/\"b in { c: c is_less_than {a,b}};
{ c: c is_less_than {a,b}} is_less_than a"/\"b
proof
let d be Element of C;
assume d in { c: c is_less_than {a,b}};
then
A9: ex c st d = c & c is_less_than {a,b};
then
A10: d [= a by A4;
d [= b by A5,A9;
hence thesis by A10,FILTER_0:7;
end;
hence thesis by A8,Th40;
end;
theorem
a = "\/"({b: b [= a}, C) & a = "/\"({c: a [= c}, C)
proof
set X = {b: b [= a}, Y = {c: a [= c};
A1: a in X;
A2: a in Y;
X is_less_than a
proof
let b;
assume b in X;
then ex c st b = c & c [= a;
hence thesis;
end;
hence a = "\/"(X,C) by A1,Th40;
a is_less_than Y
proof
let b;
assume b in Y;
then ex c st b = c & a [= c;
hence thesis;
end;
hence thesis by A2,Th41;
end;
theorem Th45:
X c= Y implies "\/"(X,C) [= "\/"(Y,C) & "/\"(Y,C) [= "/\"(X,C)
proof
assume
A1: X c= Y;
X is_less_than "\/"(Y,C)
proof
let a;
assume
A2: a in X;
Y is_less_than "\/"(Y,C) by Def21;
hence thesis by A1,A2;
end;
hence "\/"(X,C) [= "\/"(Y,C) by Def21;
"/\"(Y,C) is_less_than X
proof
let a;
assume
A3: a in X;
"/\"(Y,C) is_less_than Y by Th34;
hence thesis by A1,A3;
end;
hence thesis by Th34;
end;
theorem Th46:
"\/"(X,C) = "\/"({a: ex b st a [= b & b in X}, C) &
"/\"(X,C) = "/\"({b: ex a st a [= b & a in X}, C)
proof
set Y = {a: ex b st a [= b & b in X}, Z = {a: ex b st b [= a & b in X};
X is_less_than "\/"(Y,C)
proof
let a;
assume a in X;
then a in Y;
hence thesis by Th38;
end;
then
A1: "\/"(X,C) [= "\/"(Y,C) by Def21;
Y is_less_than "\/"(X,C)
proof
let a;
assume a in Y;
then ex b st a = b & ex c st b [= c & c in X;
then consider c such that
A2: a [= c and
A3: c in X;
c [= "\/"(X,C) by A3,Th38;
hence thesis by A2,LATTICES:7;
end;
then "\/"(Y,C) [= "\/"(X,C) by Def21;
hence "\/"(X,C) = "\/"(Y,C) by A1,LATTICES:8;
X is_greater_than "/\"(Z,C)
proof
let a;
assume a in X;
then a in Z;
hence thesis by Th38;
end;
then
A4: "/\"(Z,C) [= "/\"(X,C) by Th34;
Z is_greater_than "/\"(X,C)
proof
let a;
assume a in Z;
then ex b st a = b & ex c st c [= b & c in X;
then consider c such that
A5: c [= a and
A6: c in X;
"/\"(X,C) [= c by A6,Th38;
hence thesis by A5,LATTICES:7;
end;
then "/\"(X,C) [= "/\"(Z,C) by Th34;
hence thesis by A4,LATTICES:8;
end;
theorem
(for a st a in X ex b st a [= b & b in Y) implies "\/"(X,C) [= "\/"(Y, C )
proof
assume
A1: for a st a in X ex b st a [= b & b in Y;
X is_less_than "\/"(Y,C)
proof
let a;
assume a in X;
then consider b such that
A2: a [= b and
A3: b in Y by A1;
b [= "\/"(Y,C) by A3,Th38;
hence thesis by A2,LATTICES:7;
end;
hence thesis by Def21;
end;
theorem
X c= bool the carrier of C implies "\/"(union X, C) = "\/"({"\/"
Y where Y is Subset of C: Y in X}, C)
proof
set Z = {"\/"Y where Y is Subset of C: Y in X};
Z is_less_than "\/"(union X, C)
proof
let a;
assume a in Z;
then consider Y being Subset of C such that
A1: a = "\/"Y and
A2: Y in X;
Y c= union X by A2,ZFMISC_1:74;
hence thesis by A1,Th45;
end;
then
A3: "\/"(Z,C) [= "\/"(union X, C) by Def21;
set V = {a: ex b st a [= b & b in Z};
assume
A4: X c= bool the carrier of C;
union X c= V
proof
let x be object;
assume x in union X;
then consider Y such that
A5: x in Y and
A6: Y in X by TARSKI:def 4;
reconsider Y as Subset of C by A4,A6;
reconsider a = x as Element of C by A4,A5,A6;
A7: a [= "\/"Y by A5,Th38;
"\/"Y in Z by A6;
hence thesis by A7;
end;
then "\/"(union X, C) [= "\/"(V,C) by Th45;
then "\/"(union X, C) [= "\/"(Z,C) by Th46;
hence thesis by A3,LATTICES:8;
end;
theorem
C is 0_Lattice & Bottom C = "\/"({},C)
proof
A1: now
let a;
{} is_less_than ("\/"({},C))"/\"a;
then
A2: "\/"({},C) [= ("\/"({},C))"/\"a by Def21;
A3: ("\/"({},C))"/\"a [= "\/"({},C ) by LATTICES:6;
hence ("\/"({},C))"/\"a = "\/"({},C) by A2,LATTICES:8;
thus a"/\"("\/"({},C)) = "\/"({},C) by A2,A3,LATTICES:8;
end;
then C is lower-bounded;
hence thesis by A1,LATTICES:def 16;
end;
theorem
C is 1_Lattice & Top C = "\/"(the carrier of C, C)
proof
set j = "\/"(the carrier of C, C);
A1: now
let a;
A2: j [= j"\/"a by LATTICES:5;
A3: j"\/"a [= j by Th38;
hence j"\/"a = j by A2,LATTICES:8;
thus a"\/"j = j by A2,A3,LATTICES:8;
end;
then C is upper-bounded;
hence thesis by A1,LATTICES:def 17;
end;
theorem Th51:
C is I_Lattice implies a => b = "\/"({c: a"/\"c [= b}, C)
proof
set X = {a9: a"/\"a9 [= b};
assume
A1: C is I_Lattice;
then a"/\"(a=>b) [= b by FILTER_0:def 7;
then
A2: a=>b in X;
X is_less_than a=>b
proof
let c;
assume c in X;
then ex a9 st c = a9 & a"/\"a9 [= b;
hence c [= a=>b by A1,FILTER_0:def 7;
end;
hence thesis by A2,Th40;
end;
theorem
C is I_Lattice implies C is \/-distributive
proof
assume
A1: C is I_Lattice;
now
let X,a;
set Y = {a"/\"a9: a9 in X}, b = "\/"(X,C), c = "\/"(Y,C), Z = {b9: a"/\"
b9 [= c};
X is_less_than a=>c
proof
let b9;
assume b9 in X;
then a"/\"b9 in Y;
then a"/\"b9 [= c by Th38;
then
A2: b9 in Z;
a=>c = "\/"(Z,C) by A1,Th51;
hence thesis by A2,Th38;
end;
then b [= a=>c by Def21;
then
A3: a"/\"b [= a"/\"(a=>c) by LATTICES:9;
a"/\" (a=>c) [= c by A1,FILTER_0:def 7;
hence a"/\"b [= c by A3,LATTICES:7;
end;
hence thesis by Th33;
end;
theorem
for D being complete \/-distributive Lattice, a being Element of D holds
a "/\" "\/"(X,D) = "\/"({a"/\" b1 where b1 is Element of D: b1 in X}, D) &
"\/"(X,D) "/\" a = "\/"({b2"/\" a where b2 is Element of D: b2 in X}, D)
proof
let D be complete \/-distributive Lattice, a be Element of D;
A1: "\/"({a"/\"b where b is Element of D: b in X}, D) [= a "/\" "\/"(X,D)
by Th32;
A2: a"/\""\/"(X,D) [= "\/"({a"/\" b where b is Element of D: b in X}, D) by
Th33;
hence
a"/\""\/"(X,D) = "\/"({a"/\" b where b is Element of D: b in X}, D)
by A1,LATTICES:8;
deffunc U(Element of D) = $1"/\"a;
deffunc V(Element of D) = a"/\"$1;
defpred X[set] means $1 in X;
A3: for b being Element of D holds V(b) = U(b);
{V(b) where b is Element of D: X[b]} = {U(c) where c is Element of D: X[c]}
from FRAENKEL:sch 5(A3);
hence thesis by A1,A2,LATTICES:8;
end;
theorem
for D being complete /\-distributive Lattice, a being Element of D holds
a "\/" "/\"(X,D) = "/\"({a"\/"b1 where b1 is Element of D: b1 in X}, D) &
"/\"(X,D) "\/" a = "/\"({b2"\/" a where b2 is Element of D: b2 in X}, D)
proof
let D be complete /\-distributive Lattice, a be Element of D;
defpred X[set] means $1 in X;
A1: "/\"({a"\/"b where b is Element of D: b in X}, D) [= a "\/" "/\"(X,D)
by Th36;
A2: a"\/""/\"(X,D) [= "/\"({a"\/" b where b is Element of D: b in X}, D) by
Th35;
hence a"\/""/\"(X,D) = "/\"({a"\/"b where b is Element of D: b in X}, D)
by A1,LATTICES:8;
deffunc U(Element of D) = $1"\/"a;
deffunc V(Element of D) = a"\/"$1;
A3: for b being Element of D holds V(b) = U(b);
{V(b) where b is Element of D: X[b]} = {U(c) where c is Element of D: X[c]}
from FRAENKEL:sch 5(A3);
hence thesis by A1,A2,LATTICES:8;
end;
scheme SingleFraenkel{A()->set, B()->non empty set, P[set]}:
{A() where a is Element of B(): P[a]} = {A()}
provided
A1: ex a being Element of B() st P[a]
proof
thus {A() where a is Element of B(): P[a]} c= {A()}
proof
let x be object;
assume x in {A() where a is Element of B(): P[a]};
then ex a being Element of B() st x = A() & P[a];
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {A()};
then x = A() by TARSKI:def 1;
hence thesis by A1;
end;
scheme FuncFraenkel{B()->non empty set, C()->non empty set,
A(set)->Element of C(),f()->Function, P[set]}:
f().:{A(x) where x is Element of B(): P[x]} =
{f().A(x) where x is Element of B(): P[x]}
provided
A1: C() c= dom f()
proof
set f = f();
thus f.:{A(x) where x is Element of B(): P[x]} c=
{f.A(x) where x is Element of B(): P[x]}
proof
let y be object;
assume y in f.:{A(x) where x is Element of B(): P[x]};
then consider z being object such that
z in dom f and
A2: z in {A(x) where x is Element of B(): P[x]} and
A3: y = f.z by FUNCT_1:def 6;
ex x being Element of B() st z = A(x) & P[x] by A2;
hence thesis by A3;
end;
let y be object;
assume y in {f.A(x) where x is Element of B(): P[x]};
then consider x being Element of B() such that
A4: y = f.A(x) and
A5: P[x];
A6: A(x) in dom f by A1;
A(x) in {A(z) where z is Element of B(): P[z]} by A5;
hence thesis by A4,A6,FUNCT_1:def 6;
end;
Lm3: now
let D be non empty set, f be Function of bool D, D such that
A1: for a being Element of D holds f.{a} = a and
A2: for X being Subset-Family of D holds f.(f.:X) = f.(union X);
defpred X[object,object] means f.{$1,$2} = $2;
consider R being Relation of D such that
A3: for x,y being object holds [x,y] in R iff x in D & y in D & X[x,y]
from RELSET_1:sch 1;
A4: dom f = bool D by FUNCT_2:def 1;
A5: now
let x,y be Subset of D;
thus f.{f.x,f.y} = f.(f.:{x,y}) by A4,FUNCT_1:60
.= f.union{x,y} by A2
.= f.(x \/ y) by ZFMISC_1:75;
end;
A6: for x,y being Element of D, X being Subset of D st y in X holds
f.(X \/ {x}) = f.{f.{t,x} where t is Element of D: t in X}
proof
let x,y be Element of D, X be Subset of D such that
A7: y in X;
set Y = {{t,x} where t is Element of D: t in X};
A8: X \/ {x} = union Y
proof
thus X \/ {x} c= union Y
proof
let s be object;
assume s in X \/ {x};
then s in X & X c= D or s in {x} by XBOOLE_0:def 3;
then s in X & s is Element of D or s = x by TARSKI:def 1;
then s in {s,x} & {s,x} in Y or s in {y,x} & {y,x} in
Y by A7,TARSKI:def 2;
hence thesis by TARSKI:def 4;
end;
let s be object;
assume s in union Y;
then consider Z being set such that
A9: s in Z and
A10: Z in Y by TARSKI:def 4;
consider t being Element of D such that
A11: Z = {t,x} and
A12: t in X by A10;
s = t or s = x & x in {x} by A9,A11,TARSKI:def 1,def 2;
hence thesis by A12,XBOOLE_0:def 3;
end;
Y c= bool D
proof
let s be object;
reconsider ss=s as set by TARSKI:1;
assume s in Y;
then ss c= X \/ {x} by A8,ZFMISC_1:74;
then ss c= D by XBOOLE_1:1;
hence thesis;
end;
then reconsider Y as Subset-Family of D;
defpred X[set] means $1 in X;
deffunc U(Element of D) = {$1,x};
A13: bool D c= dom f by FUNCT_2:def 1;
f.:{U(t) where t is Element of D: X[t]} =
{f.U(t) where t is Element of D: X[t]} from FuncFraenkel(A13);
then f.union Y = f.{f.{t,x} where t is Element of D: t in X} by A2;
hence thesis by A8;
end;
A14: R is_reflexive_in D
proof
let x be object;
assume
A15: x in D;
then x = f.{x} by A1
.= f.{x,x} by ENUMSET1:29;
hence thesis by A3,A15;
end;
A16: R is_antisymmetric_in D
proof
let x,y be object;
assume that x in D and y in D and
A17: [x,y] in R and
A18: [y,x] in R;
f.{x,y} = y by A3,A17;
hence thesis by A3,A18;
end;
A19: R is_transitive_in D
proof
let x,y,z be object;
assume that
A20: x in D and
A21: y in D and
A22: z in D and
A23: [x,y] in R and
A24: [y,z] in R;
reconsider a = x, b = y, c = z as Element of D by A20,A21,A22;
A25: f.{x,y} = y by A3,A23;
A26: f.{y,z} = z by A3,A24;
then f.{a,c} = f.{f.{a},f.{b,c}} by A1
.= f.({a}\/{b,c}) by A5
.= f.{a,b,c} by ENUMSET1:2
.= f.({a,b}\/{c}) by ENUMSET1:3
.= f.{f.{a,b},f.{c}} by A5
.= c by A1,A25,A26;
hence thesis by A3;
end;
A27: dom R = D by A14,ORDERS_1:13;
field R = D by A14,ORDERS_1:13;
then reconsider R as Order of D
by A14,A16,A19,A27,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 16;
set A = RelStr(#D,R#);
A is complete
proof
let X;
reconsider Y = X /\ D as Subset of D by XBOOLE_1:17;
reconsider a = (f.Y) as Element of A;
take a;
thus X is_<=_than a
proof
let b be Element of A;
assume b in X;
then b in Y by XBOOLE_0:def 4;
then {b} \/ Y = Y by ZFMISC_1:40;
then a = f.{f.{b},a} by A5
.= f.{b,a} by A1;
hence [b,a] in the InternalRel of A by A3;
end;
let b be Element of A such that
A28: X is_<=_than b;
A29: f.{a,b} = f.{a,f.{b}} by A1
.= f.(Y \/ {b}) by A5;
now per cases;
suppose
A30: Y <> {};
set s = the Element of Y;
reconsider s as Element of D by A30,TARSKI:def 3;
deffunc U(Element of D) = f.{$1,b};
deffunc V(Element of D) = b;
defpred X[set] means $1 in Y;
A31: for t being Element of D st X[t] holds U(t) = V(t)
proof
let t be Element of D;
reconsider s = t as Element of A;
reconsider y = b as Element of D;
assume t in Y;
then t in X by XBOOLE_0:def 4;
then s <= b by A28;
then [t,y] in R;
hence thesis by A3;
end;
A32: s in Y by A30;
then
A33: ex t being Element of D st X[t];
{U(t) where t is Element of D: X[t]}
= {V(t) where t is Element of D: X[t]} from FRAENKEL:sch 6(A31)
.= {b where t is Element of D: X[t]}
.= {b} from SingleFraenkel(A33);
hence f.{a,b} = f.{b} by A6,A29,A32
.= b by A1;
end;
suppose Y = {};
hence f.{a,b} = b by A1,A29;
end;
end;
hence [a,b] in the InternalRel of A by A3;
end;
then reconsider A as complete strict non empty Poset;
take L = latt A;
A34: A is with_suprema with_infima by Th12;
then
A35: A = LattPOSet L by Def15;
hence carr(L) = D;
let X be Subset of L;
reconsider Y = X as Subset of D by A35;
reconsider a = f.Y as Element of LattPOSet L by A34,Def15;
set p = %a;
X is_<=_than a
proof
let b be Element of LattPOSet L;
reconsider y = b as Element of D by A34,Def15;
assume b in X;
then
A36: X = {b} \/ X by ZFMISC_1:40;
f.{y,f.Y} = f.{f.{y},f.Y} by A1
.= a by A5,A36;
hence [b,a] in the InternalRel of LattPOSet L by A3,A35;
end;
then
A37: X is_less_than p by Th31;
now
let q be Element of L;
reconsider y = q as Element of D by A35;
reconsider b = y as Element of LattPOSet L;
assume X is_less_than q;
then
A38: X is_<=_than q% by Th30;
A39: f.{f.Y,b} = f.{f.Y,f.{y}} by A1
.= f.(Y \/ {b}) by A5;
now per cases;
suppose
A40: Y <> {};
set s = the Element of Y;
reconsider s as Element of D by A40,TARSKI:def 3;
deffunc U(Element of D) = f.{$1,b};
deffunc V(Element of D) = b;
defpred X[set] means $1 in Y;
A41: for t being Element of D st X[t] holds U(t) = V(t)
proof
let t be Element of D;
reconsider s = t as Element of LattPOSet L by A34,Def15;
assume t in Y;
then s <= b by A38;
then [t,y] in R by A35;
hence thesis by A3;
end;
A42: s in Y by A40;
then
A43: ex t being Element of D st X[t];
{U(t) where t is Element of D: X[t]}
= {V(t) where t is Element of D: X[t]} from FRAENKEL:sch 6(A41)
.= {b where t is Element of D: X[t]}
.= {b} from SingleFraenkel(A43);
hence f.{a,b} = f.{b} by A6,A39,A42
.= b by A1;
end;
suppose Y = {};
hence f.{a,b} = b by A1,A39;
end;
end;
then [a,b] in the InternalRel of LattPOSet L by A3,A35;
then
A44: a <= b;
A45: p% = p;
q% = b;
hence p [= q by A44,A45,Th7;
end;
hence "\/"X = f.X by A37,Def21;
end;
theorem
for D being non empty set, f being Function of bool D, D st
(for a being Element of D holds f.{a} = a) &
for X being Subset-Family of D holds f.(f.:X) = f.(union X)
ex L being complete strict Lattice st the carrier of L = D &
for X being Subset of L holds "\/" X = f.X by Lm3;