:: Definitions and Properties of the Join and Meet of Subsets
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDERS_2, SUBSET_1, YELLOW_0, XXREAL_0, EQREL_1, LATTICE3,
LATTICES, SETFAM_1, XBOOLE_0, RELAT_2, WAYBEL_0, TARSKI, STRUCT_0,
ORDINAL2, REWRITE1, YELLOW_1, ZFMISC_1, RELAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, LATTICE3, YELLOW_0, DOMAIN_1, STRUCT_0,
ORDERS_2, YELLOW_1, WAYBEL_0, YELLOW_3;
constructors DOMAIN_1, LATTICE3, YELLOW_1, YELLOW_3, WAYBEL_0;
registrations STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2;
requirements SUBSET, BOOLE;
definitions LATTICE3, TARSKI, WAYBEL_0, XBOOLE_0;
expansions LATTICE3, TARSKI, WAYBEL_0;
theorems LATTICE3, ORDERS_2, TARSKI, WAYBEL_0, YELLOW_0, YELLOW_1, YELLOW_2,
YELLOW_3, XBOOLE_0;
begin :: Preliminaries
theorem Th1:
for L being RelStr, X being set, a being Element of L st a in X &
ex_sup_of X,L holds a <= "\/"(X,L)
proof
let L be RelStr, X be set, a be Element of L such that
A1: a in X and
A2: ex_sup_of X,L;
X is_<=_than "\/"(X, L) by A2,YELLOW_0:def 9;
hence thesis by A1;
end;
theorem Th2:
for L being RelStr, X being set, a being Element of L st a in X &
ex_inf_of X,L holds "/\"(X,L) <= a
proof
let L be RelStr, X be set, a be Element of L such that
A1: a in X and
A2: ex_inf_of X,L;
X is_>=_than "/\"(X, L) by A2,YELLOW_0:def 10;
hence thesis by A1;
end;
definition
let L be RelStr, A, B be Subset of L;
pred A is_finer_than B means
for a being Element of L st a in A ex b
being Element of L st b in B & a <= b;
pred B is_coarser_than A means
for b being Element of L st b in B ex
a being Element of L st a in A & a <= b;
end;
definition
let L be non empty reflexive RelStr, A, B be Subset of L;
redefine pred A is_finer_than B; :: redefines is_finer_than (YELLOW_4, definition)
reflexivity
proof
let A be Subset of L;
let a be Element of L such that
A1: a in A;
take b = a;
thus b in A & a <= b by A1;
end;
redefine pred B is_coarser_than A; :: redefines is_coarser_than (YELLOW_4, definition)
reflexivity
proof
let A be Subset of L;
let a be Element of L such that
A2: a in A;
take b = a;
thus b in A & b <= a by A2;
end;
end;
theorem
for L being RelStr, B being Subset of L holds {}L is_finer_than B;
theorem
for L being transitive RelStr, A, B, C being Subset of L st A
is_finer_than B & B is_finer_than C holds A is_finer_than C
proof
let L be transitive RelStr, A, B, C be Subset of L such that
A1: A is_finer_than B and
A2: B is_finer_than C;
let a be Element of L;
assume a in A;
then consider b being Element of L such that
A3: b in B and
A4: a <= b by A1;
consider c being Element of L such that
A5: c in C & b <= c by A2,A3;
take c;
thus thesis by A4,A5,ORDERS_2:3;
end;
theorem
for L being RelStr, A, B being Subset of L st B is_finer_than A & A is
lower holds B c= A
proof
let L be RelStr, A, B be Subset of L such that
A1: B is_finer_than A and
A2: A is lower;
let a be object;
assume
A3: a in B;
then reconsider a1 = a as Element of L;
ex b being Element of L st b in A & a1 <= b by A1,A3;
hence thesis by A2;
end;
theorem
for L being RelStr, A being Subset of L holds {}L is_coarser_than A;
theorem
for L being transitive RelStr, A, B, C being Subset of L st C
is_coarser_than B & B is_coarser_than A holds C is_coarser_than A
proof
let L be transitive RelStr, A, B, C be Subset of L such that
A1: C is_coarser_than B and
A2: B is_coarser_than A;
let c be Element of L;
assume c in C;
then consider b being Element of L such that
A3: b in B and
A4: b <= c by A1;
consider a being Element of L such that
A5: a in A & a <= b by A2,A3;
take a;
thus thesis by A4,A5,ORDERS_2:3;
end;
theorem
for L being RelStr, A, B being Subset of L st A is_coarser_than B & B
is upper holds A c= B
proof
let L be RelStr, A, B be Subset of L such that
A1: A is_coarser_than B and
A2: B is upper;
let a be object;
assume
A3: a in A;
then reconsider a1 = a as Element of L;
ex b being Element of L st b in B & b <= a1 by A1,A3;
hence thesis by A2;
end;
begin :: The Join of Subsets
definition
let L be non empty RelStr, D1, D2 be Subset of L;
func D1 "\/" D2 -> Subset of L equals
{ x "\/" y where x, y is Element of L
: x in D1 & y in D2 };
coherence
proof
{ x "\/" y where x, y is Element of L : x in D1 & y in D2 } c= the
carrier of L
proof
let q be object;
assume q in { x "\/" y where x, y is Element of L : x in D1 & y in D2 };
then ex a, b being Element of L st q = a "\/" b & a in D1 & b in D2;
hence thesis;
end;
hence thesis;
end;
end;
definition
let L be with_suprema antisymmetric RelStr, D1, D2 be Subset of L;
redefine func D1 "\/" D2; :: redefines "\/" (YELLOW_4, definition)
commutativity
proof
let D1, D2 be Subset of L;
thus D1 "\/" D2 c= D2 "\/" D1
proof
let q be object;
assume q in D1 "\/" D2;
then ex x, y being Element of L st q = x "\/" y & x in D1 & y in D2;
hence thesis;
end;
let q be object;
assume q in D2 "\/" D1;
then ex x, y being Element of L st q = x "\/" y & x in D2 & y in D1;
hence thesis;
end;
end;
theorem
for L being non empty RelStr, X being Subset of L holds X "\/" {}L = {}
proof
let L be non empty RelStr, X be Subset of L;
thus X "\/" {}L c= {}
proof
let a be object;
assume a in X "\/" {}L;
then ex s,t be Element of L st a = s "\/" t & s in X & t in {}L;
hence thesis;
end;
thus thesis;
end;
theorem
for L being non empty RelStr, X, Y being Subset of L, x, y being
Element of L st x in X & y in Y holds x "\/" y in X "\/" Y;
theorem
for L being antisymmetric with_suprema RelStr for A being Subset of L,
B being non empty Subset of L holds A is_finer_than A "\/" B
proof
let L be antisymmetric with_suprema RelStr, A be Subset of L, B be non empty
Subset of L;
let q be Element of L such that
A1: q in A;
set b = the Element of B;
take q "\/" b;
thus q "\/" b in A "\/" B by A1;
thus thesis by YELLOW_0:22;
end;
theorem
for L being antisymmetric with_suprema RelStr, A, B being Subset of L
holds A "\/" B is_coarser_than A
proof
let L be antisymmetric with_suprema RelStr, A, B be Subset of L;
let q be Element of L;
assume q in A "\/" B;
then consider x, y being Element of L such that
A1: q = x "\/" y and
A2: x in A and
y in B;
take x;
thus x in A by A2;
thus thesis by A1,YELLOW_0:22;
end;
theorem
for L being antisymmetric reflexive with_suprema RelStr for A being
Subset of L holds A c= A "\/" A
proof
let L be antisymmetric reflexive with_suprema RelStr, A be Subset of L;
let q be object;
assume
A1: q in A;
then reconsider A1 = A as non empty Subset of L;
reconsider q1 = q as Element of A1 by A1;
q1 <= q1;
then q1 = q1 "\/" q1 by YELLOW_0:24;
hence thesis;
end;
theorem
for L being with_suprema antisymmetric transitive RelStr for D1, D2,
D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)
proof
let L be with_suprema antisymmetric transitive RelStr, D1, D2, D3 be Subset
of L;
thus (D1 "\/" D2) "\/" D3 c= D1 "\/" (D2 "\/" D3)
proof
let q be object;
assume q in (D1 "\/" D2) "\/" D3;
then consider a1, b1 being Element of L such that
A1: q = a1 "\/" b1 and
A2: a1 in D1 "\/" D2 and
A3: b1 in D3;
consider a11, b11 being Element of L such that
A4: a1 = a11 "\/" b11 and
A5: a11 in D1 and
A6: b11 in D2 by A2;
b11 "\/" b1 in D2 "\/" D3 & q = a11 "\/" (b11 "\/" b1) by A1,A3,A4,A6,
LATTICE3:14;
hence thesis by A5;
end;
let q be object;
assume q in D1 "\/" (D2 "\/" D3);
then consider a1, b1 being Element of L such that
A7: q = a1 "\/" b1 & a1 in D1 and
A8: b1 in D2 "\/" D3;
consider a11, b11 being Element of L such that
A9: b1 = a11 "\/" b11 & a11 in D2 and
A10: b11 in D3 by A8;
a1 "\/" a11 in D1 "\/" D2 & q = a1 "\/" a11 "\/" b11 by A7,A9,LATTICE3:14;
hence thesis by A10;
end;
registration
let L be non empty RelStr, D1, D2 be non empty Subset of L;
cluster D1 "\/" D2 -> non empty;
coherence
proof
consider b being object such that
A1: b in D2 by XBOOLE_0:def 1;
reconsider b as Element of D2 by A1;
consider a being object such that
A2: a in D1 by XBOOLE_0:def 1;
reconsider a as Element of D1 by A2;
a "\/" b in { x "\/" y where x, y is Element of L : x in D1 & y in D2 };
hence thesis;
end;
end;
registration
let L be with_suprema transitive antisymmetric RelStr, D1, D2 be directed
Subset of L;
cluster D1 "\/" D2 -> directed;
coherence
proof
let a, b be Element of L;
set X = D1 "\/" D2;
assume that
A1: a in X and
A2: b in X;
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "\/" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: y <= z2 & t <= z2 by A5,A8,WAYBEL_0:def 1;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: x <= z1 & s <= z1 by A4,A7,WAYBEL_0:def 1;
take z = z1 "\/" z2;
thus z in X by A11,A9;
thus thesis by A3,A6,A12,A10,YELLOW_3:3;
end;
end;
registration
let L be with_suprema transitive antisymmetric RelStr, D1, D2 be filtered
Subset of L;
cluster D1 "\/" D2 -> filtered;
coherence
proof
let a, b be Element of L;
set X = D1 "\/" D2;
assume that
A1: a in X and
A2: b in X;
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "\/" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: y >= z2 & t >= z2 by A5,A8,WAYBEL_0:def 2;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: x >= z1 & s >= z1 by A4,A7,WAYBEL_0:def 2;
take z = z1 "\/" z2;
thus z in X by A11,A9;
thus thesis by A3,A6,A12,A10,YELLOW_3:3;
end;
end;
registration
let L be with_suprema Poset, D1, D2 be upper Subset of L;
cluster D1 "\/" D2 -> upper;
coherence
proof
set X = D1 "\/" D2;
let a, b be Element of L such that
A1: a in X and
A2: a <= b;
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
A6: ex xx being Element of L st x <= xx & y <= xx & for c being Element of
L st x <= c & y <= c holds xx <= c by LATTICE3:def 10;
then x <= x "\/" y by LATTICE3:def 13;
then x <= b by A2,A3,YELLOW_0:def 2;
then
A7: b in D1 by A4,WAYBEL_0:def 20;
y <= x "\/" y by A6,LATTICE3:def 13;
then y <= b by A2,A3,YELLOW_0:def 2;
then
A8: b in D2 by A5,WAYBEL_0:def 20;
b <= b;
then b = b "\/" b by YELLOW_0:24;
hence thesis by A7,A8;
end;
end;
theorem Th15:
for L being non empty RelStr, Y being Subset of L, x being
Element of L holds {x} "\/" Y = {x "\/" y where y is Element of L: y in Y}
proof
let L be non empty RelStr, Y be Subset of L, x be Element of L;
thus {x} "\/" Y c= {x "\/" y where y is Element of L: y in Y}
proof
let q be object;
assume q in {x} "\/" Y;
then consider s, t being Element of L such that
A1: q = s "\/" t and
A2: s in {x} and
A3: t in Y;
s = x by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let q be object;
assume q in {x "\/" y where y is Element of L: y in Y};
then
A4: ex y being Element of L st q = x "\/" y & y in Y;
x in {x} by TARSKI:def 1;
hence thesis by A4;
end;
theorem
for L being non empty RelStr, A, B, C being Subset of L holds A "\/" (
B \/ C) = (A "\/" B) \/ (A "\/" C)
proof
let L be non empty RelStr, A, B, C be Subset of L;
thus A "\/" (B \/ C) c= (A "\/" B) \/ (A "\/" C)
proof
let q be object;
assume q in A "\/" (B \/ C);
then consider a, y being Element of L such that
A1: q = a "\/" y & a in A and
A2: y in B \/ C;
y in B or y in C by A2,XBOOLE_0:def 3;
then q in A "\/" B or q in A "\/" C by A1;
hence thesis by XBOOLE_0:def 3;
end;
let q be object such that
A3: q in (A "\/" B) \/ (A "\/" C);
per cases by A3,XBOOLE_0:def 3;
suppose
q in A "\/" B;
then consider a, b being Element of L such that
A4: q = a "\/" b & a in A and
A5: b in B;
b in B \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
suppose
q in A "\/" C;
then consider a, b being Element of L such that
A6: q = a "\/" b & a in A and
A7: b in C;
b in B \/ C by A7,XBOOLE_0:def 3;
hence thesis by A6;
end;
end;
theorem
for L being antisymmetric reflexive with_suprema RelStr for A, B, C
being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)
proof
let L be antisymmetric reflexive with_suprema RelStr, A, B, C be Subset of L;
let q be object such that
A1: q in A \/ (B "\/" C);
per cases by A1,XBOOLE_0:def 3;
suppose
A2: q in A;
then reconsider q1 = q as Element of L;
q1 <= q1;
then
A3: q1 = q1 "\/" q1 by YELLOW_0:24;
q1 in A \/ B & q1 in A \/ C by A2,XBOOLE_0:def 3;
hence thesis by A3;
end;
suppose
q in B "\/" C;
then consider b, c being Element of L such that
A4: q = b "\/" c and
A5: b in B & c in C;
b in A \/ B & c in A \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
end;
theorem
for L being antisymmetric with_suprema RelStr, A being upper Subset of
L for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
proof
let L be antisymmetric with_suprema RelStr, A be upper Subset of L, B, C be
Subset of L;
let q be object;
assume q in (A \/ B) "\/" (A \/ C);
then consider x, y being Element of L such that
A1: q = x "\/" y and
A2: x in A \/ B & y in A \/ C;
A3: x <= x "\/" y by YELLOW_0:22;
A4: y <= x "\/" y by YELLOW_0:22;
per cases by A2,XBOOLE_0:def 3;
suppose
x in A & y in A;
then q in A by A1,A3,WAYBEL_0:def 20;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in A & y in C;
then q in A by A1,A3,WAYBEL_0:def 20;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in B & y in A;
then q in A by A1,A4,WAYBEL_0:def 20;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in B & y in C;
then x "\/" y in B "\/" C;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
Lm1: now
let L be non empty RelStr, x, y be Element of L;
thus {a "\/" b where a, b is Element of L : a in {x} & b in {y}} = {x "\/" y
}
proof
thus {a "\/" b where a, b is Element of L : a in {x} & b in {y}} c= {x
"\/" y}
proof
let q be object;
assume q in {a "\/" b where a, b is Element of L : a in {x} & b in {y}};
then consider u,v being Element of L such that
A1: q = u "\/" v and
A2: u in {x} & v in {y};
u = x & v = y by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let q be object;
assume q in {x "\/" y};
then
A3: q = x "\/" y by TARSKI:def 1;
x in {x} & y in {y} by TARSKI:def 1;
hence thesis by A3;
end;
end;
Lm2: now
let L be non empty RelStr, x, y, z be Element of L;
thus {a "\/" b where a, b is Element of L : a in {x} & b in {y,z}} = {x "\/"
y, x "\/" z}
proof
thus {a "\/" b where a, b is Element of L : a in {x} & b in {y,z}} c= {x
"\/" y, x "\/" z}
proof
let q be object;
assume
q in {a "\/" b where a, b is Element of L : a in {x} & b in {y,z }};
then consider u,v being Element of L such that
A1: q = u "\/" v and
A2: u in {x} and
A3: v in {y,z};
A4: v = y or v = z by A3,TARSKI:def 2;
u = x by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let q be object;
A5: z in {y,z} by TARSKI:def 2;
assume q in {x "\/" y, x "\/" z};
then
A6: q = x "\/" y or q = x "\/" z by TARSKI:def 2;
x in {x} & y in {y,z} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
end;
theorem
for L being non empty RelStr, x, y being Element of L holds {x} "\/" {
y} = {x "\/" y} by Lm1;
theorem
for L being non empty RelStr, x, y, z being Element of L holds {x}
"\/" {y,z} = {x "\/" y, x "\/" z} by Lm2;
theorem
for L being non empty RelStr, X1, X2, Y1, Y2 being Subset of L st X1
c= Y1 & X2 c= Y2 holds X1 "\/" X2 c= Y1 "\/" Y2
proof
let L be non empty RelStr, X1, X2, Y1, Y2 be Subset of L such that
A1: X1 c= Y1 & X2 c= Y2;
let q be object;
assume q in X1 "\/" X2;
then ex x, y being Element of L st q = x "\/" y & x in X1 & y in X2;
hence thesis by A1;
end;
theorem
for L being with_suprema reflexive antisymmetric RelStr for D being
Subset of L, x being Element of L st x is_<=_than D holds {x} "\/" D = D
proof
let L be with_suprema reflexive antisymmetric RelStr, D be Subset of L, x be
Element of L such that
A1: x is_<=_than D;
A2: {x} "\/" D = { x "\/" y where y is Element of L : y in D } by Th15;
thus {x} "\/" D c= D
proof
let q be object;
assume q in {x} "\/" D;
then consider y being Element of L such that
A3: q = x "\/" y and
A4: y in D by A2;
x <= y by A1,A4;
hence thesis by A3,A4,YELLOW_0:24;
end;
let q be object;
assume
A5: q in D;
then reconsider D1 = D as non empty Subset of L;
reconsider y = q as Element of D1 by A5;
x <= y by A1;
then q = x "\/" y by YELLOW_0:24;
hence thesis by A2;
end;
theorem
for L being with_suprema antisymmetric RelStr for D being Subset of L,
x being Element of L holds x is_<=_than {x} "\/" D
proof
let L be with_suprema antisymmetric RelStr, D be Subset of L, x be Element
of L;
let b be Element of L;
A1: {x} "\/" D = { x "\/" h where h is Element of L : h in D } by Th15;
assume b in {x} "\/" D;
then consider h being Element of L such that
A2: b = x "\/" h and
h in D by A1;
ex w being Element of L st x <= w & h <= w & for c being Element of L st
x <= c & h <= c holds w <= c by LATTICE3:def 10;
hence thesis by A2,LATTICE3:def 13;
end;
theorem
for L being with_suprema Poset, X being Subset of L, x being Element
of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds x "\/" inf X <= inf ({x}
"\/" X)
proof
let L be with_suprema Poset, X be Subset of L, x be Element of L such that
A1: ex_inf_of {x} "\/" X,L and
A2: ex_inf_of X,L;
A3: {x} "\/" X = {x "\/" y where y is Element of L : y in X} by Th15;
{x} "\/" X is_>=_than x "\/" inf X
proof
let q be Element of L;
assume q in {x} "\/" X;
then consider y being Element of L such that
A4: q = x "\/" y and
A5: y in X by A3;
x <= x & y >= inf X by A2,A5,Th2;
hence thesis by A4,YELLOW_3:3;
end;
hence thesis by A1,YELLOW_0:def 10;
end;
theorem Th25:
for L being complete transitive antisymmetric non empty RelStr
for A being Subset of L, B being non empty Subset of L holds A is_<=_than sup (
A "\/" B)
proof
let L be complete transitive antisymmetric non empty RelStr, A be Subset
of L, B be non empty Subset of L;
set b = the Element of B;
let x be Element of L;
assume x in A;
then
A1: x "\/" b in A "\/" B;
ex xx being Element of L st x <= xx & b <= xx & for c being Element of L
st x <= c & b <= c holds xx <= c by LATTICE3:def 10;
then
A2: x <= x "\/" b by LATTICE3:def 13;
ex_sup_of A "\/" B,L by YELLOW_0:17;
then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
then x "\/" b <= sup (A "\/" B) by A1;
hence thesis by A2,YELLOW_0:def 2;
end;
theorem
for L being with_suprema transitive antisymmetric RelStr for a, b
being Element of L, A, B being Subset of L st a is_<=_than A & b is_<=_than B
holds a "\/" b is_<=_than A "\/" B
proof
let L be with_suprema transitive antisymmetric RelStr, a, b be Element of L,
A, B be Subset of L such that
A1: a is_<=_than A & b is_<=_than B;
let q be Element of L;
assume q in A "\/" B;
then consider x, y being Element of L such that
A2: q = x "\/" y and
A3: x in A & y in B;
a <= x & b <= y by A1,A3;
hence thesis by A2,YELLOW_3:3;
end;
theorem Th27:
for L being with_suprema transitive antisymmetric RelStr for a,
b being Element of L, A, B being Subset of L st a is_>=_than A & b is_>=_than B
holds a "\/" b is_>=_than A "\/" B
proof
let L be with_suprema transitive antisymmetric RelStr, a, b be Element of L,
A, B be Subset of L such that
A1: a is_>=_than A & b is_>=_than B;
let q be Element of L;
assume q in A "\/" B;
then consider x, y being Element of L such that
A2: q = x "\/" y and
A3: x in A & y in B;
a >= x & b >= y by A1,A3;
hence thesis by A2,YELLOW_3:3;
end;
theorem
for L being complete non empty Poset for A, B being non empty Subset
of L holds sup (A "\/" B) = sup A "\/" sup B
proof
let L be complete non empty Poset, A, B be non empty Subset of L;
B is_<=_than sup (A "\/" B) by Th25;
then
A1: sup B <= sup (A "\/" B) by YELLOW_0:32;
A is_<=_than sup (A "\/" B) by Th25;
then sup A <= sup (A "\/" B) by YELLOW_0:32;
then
A2: sup A "\/" sup B <= sup (A "\/" B) "\/" sup (A "\/" B) by A1,YELLOW_3:3;
A is_<=_than sup A & B is_<=_than sup B by YELLOW_0:32;
then ex_sup_of A "\/" B,L & A "\/" B is_<=_than sup A "\/" sup B by Th27,
YELLOW_0:17;
then
A3: sup (A "\/" B) <= sup A "\/" sup B by YELLOW_0:def 9;
sup (A "\/" B) <= sup (A "\/" B);
then sup (A "\/" B) "\/" sup (A "\/" B) = sup (A "\/" B) by YELLOW_0:24;
hence thesis by A3,A2,ORDERS_2:2;
end;
theorem Th29:
for L being with_suprema antisymmetric RelStr for X being Subset
of L, Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
proof
let L be with_suprema antisymmetric RelStr, X be Subset of L, Y be non empty
Subset of L;
consider y being object such that
A1: y in Y by XBOOLE_0:def 1;
reconsider y as Element of Y by A1;
let q be object;
assume
A2: q in X;
then reconsider X1 = X as non empty Subset of L;
reconsider x = q as Element of X1 by A2;
ex s being Element of L st x <= s & y <= s & for c being Element of L st
x <= c & y <= c holds s <= c by LATTICE3:def 10;
then
A3: x <= x "\/" y by LATTICE3:def 13;
downarrow (X "\/" Y) = {s where s is Element of L: ex y being Element of
L st s <= y & y in X "\/" Y} & x "\/" y in X1 "\/" Y by WAYBEL_0:14;
hence thesis by A3;
end;
theorem
for L being with_suprema Poset for x, y being Element of InclPoset Ids
L for X, Y being Subset of L st x = X & y = Y holds x "\/" y = downarrow (X
"\/" Y)
proof
let L be with_suprema Poset, x, y be Element of InclPoset Ids L, X, Y be
Subset of L such that
A1: x = X and
A2: y = Y;
reconsider X1 = X, Y1 = Y as non empty directed Subset of L by A1,A2,
YELLOW_2:41;
reconsider d = downarrow (X1 "\/" Y1) as Element of InclPoset Ids L by
YELLOW_2:41;
Y c= d by Th29;
then
A3: y <= d by A2,YELLOW_1:3;
X c= d by Th29;
then x <= d by A1,YELLOW_1:3;
then d <= d & x "\/" y <= d "\/" d by A3,YELLOW_3:3;
then x "\/" y <= d by YELLOW_0:24;
hence x "\/" y c= downarrow (X "\/" Y) by YELLOW_1:3;
consider Z being Subset of L such that
A4: Z = {z where z is Element of L: z in x or z in y or ex a, b being
Element of L st a in x & b in y & z = a "\/" b} and
ex_sup_of {x,y},InclPoset(Ids L) and
A5: x "\/" y = downarrow Z by YELLOW_2:44;
X "\/" Y c= Z
proof
let q be object;
assume q in X "\/" Y;
then ex s, t being Element of L st q = s "\/" t & s in X & t in Y;
hence thesis by A1,A2,A4;
end;
hence thesis by A5,YELLOW_3:6;
end;
theorem
for L being non empty RelStr, D being Subset of [:L,L:] holds union {X
where X is Subset of L: ex x being Element of L st X = {x} "\/" proj2 D & x in
proj1 D} = proj1 D "\/" proj2 D
proof
let L be non empty RelStr, D be Subset of [:L,L:];
set D1 = proj1 D, D2 = proj2 D;
defpred P[set] means ex x being Element of L st $1 = {x} "\/" proj2 D & x in
proj1 D;
thus union {X where X is Subset of L: P[X]} c= D1 "\/" D2
proof
let q be object;
assume q in union {X where X is Subset of L: P[X]};
then consider w being set such that
A1: q in w and
A2: w in {X where X is Subset of L: P[X]} by TARSKI:def 4;
consider e being Subset of L such that
A3: w = e and
A4: P[e] by A2;
consider p being Element of L such that
A5: e = {p} "\/" D2 and
A6: p in D1 by A4;
{p} "\/" D2 = { p "\/" y where y is Element of L : y in D2 } by Th15;
then ex y being Element of L st q = p "\/" y & y in D2 by A1,A3,A5;
hence thesis by A6;
end;
let q be object;
assume q in D1 "\/" D2;
then consider x, y being Element of L such that
A7: q = x "\/" y and
A8: x in D1 and
A9: y in D2;
{x} "\/" D2 = { x "\/" d where d is Element of L : d in D2 } by Th15;
then
A10: q in {x} "\/" D2 by A7,A9;
{x} "\/" D2 in {X where X is Subset of L: P[X]} by A8;
hence thesis by A10,TARSKI:def 4;
end;
theorem Th32:
for L being transitive antisymmetric with_suprema RelStr for D1,
D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c=
downarrow (D1 "\/" D2)
proof
let L be transitive antisymmetric with_suprema RelStr, D1, D2 be Subset of L;
A1: downarrow ((downarrow D1) "\/" (downarrow D2)) = {x where x is Element
of L: ex t being Element of L st x <= t & t in (downarrow D1) "\/" (downarrow
D2)} by WAYBEL_0:14;
let y be object;
assume y in downarrow ((downarrow D1) "\/" (downarrow D2));
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st x <= t & t in (downarrow D1) "\/" (
downarrow D2) by A1;
consider x1 being Element of L such that
A4: x <= x1 and
A5: x1 in (downarrow D1) "\/" (downarrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "\/" b and
A7: a in downarrow D1 and
A8: b in downarrow D2 by A5;
downarrow D2 = {s2 where s2 is Element of L: ex z being Element of L st
s2 <= z & z in D2} by WAYBEL_0:14;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st B1 <= z & z in D2 by A8;
consider b1 being Element of L such that
A11: B1 <= b1 and
A12: b1 in D2 by A10;
downarrow D1 = {s1 where s1 is Element of L: ex z being Element of L st
s1 <= z & z in D1} by WAYBEL_0:14;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st A1 <= z & z in D1 by A7;
consider a1 being Element of L such that
A15: A1 <= a1 and
A16: a1 in D1 by A14;
x1 <= a1 "\/" b1 by A6,A13,A9,A15,A11,YELLOW_3:3;
then
A17: downarrow (D1 "\/" D2) = {s where s is Element of L: ex z being Element
of L st s <= z & z in D1 "\/" D2} & x <= a1 "\/" b1 by A4,ORDERS_2:3
,WAYBEL_0:14;
a1 "\/" b1 in D1 "\/" D2 by A16,A12;
hence thesis by A2,A17;
end;
theorem
for L being with_suprema Poset, D1, D2 being Subset of L holds
downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
proof
let L be with_suprema Poset, D1, D2 be Subset of L;
A1: downarrow (D1 "\/" D2) = {s where s is Element of L: ex z being Element
of L st s <= z & z in D1 "\/" D2} by WAYBEL_0:14;
thus downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2
) by Th32;
let q be object;
assume q in downarrow (D1 "\/" D2);
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st s <= z & z in D1 "\/" D2 by A1;
A4: downarrow ((downarrow D1) "\/" (downarrow D2)) = {x where x is Element
of L: ex t being Element of L st x <= t & t in (downarrow D1) "\/" (downarrow
D2)} by WAYBEL_0:14;
A5: D1 is Subset of downarrow D1 & D2 is Subset of downarrow D2 by WAYBEL_0:16;
consider x being Element of L such that
A6: s <= x and
A7: x in D1 "\/" D2 by A3;
ex a, b being Element of L st x = a "\/" b & a in D1 & b in D2 by A7;
then x in (downarrow D1) "\/" (downarrow D2) by A5;
hence thesis by A4,A2,A6;
end;
theorem Th34:
for L being transitive antisymmetric with_suprema RelStr for D1,
D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow
(D1 "\/" D2)
proof
let L be transitive antisymmetric with_suprema RelStr, D1, D2 be Subset of L;
A1: uparrow ((uparrow D1) "\/" (uparrow D2)) = {x where x is Element of L:
ex t being Element of L st x >= t & t in (uparrow D1) "\/" (uparrow D2)} by
WAYBEL_0:15;
let y be object;
assume y in uparrow ((uparrow D1) "\/" (uparrow D2));
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st x >= t & t in (uparrow D1) "\/" (uparrow
D2) by A1;
consider x1 being Element of L such that
A4: x >= x1 and
A5: x1 in (uparrow D1) "\/" (uparrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "\/" b and
A7: a in uparrow D1 and
A8: b in uparrow D2 by A5;
uparrow D2 = {s2 where s2 is Element of L: ex z being Element of L st s2
>= z & z in D2} by WAYBEL_0:15;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st B1 >= z & z in D2 by A8;
consider b1 being Element of L such that
A11: B1 >= b1 and
A12: b1 in D2 by A10;
uparrow D1 = {s1 where s1 is Element of L: ex z being Element of L st s1
>= z & z in D1} by WAYBEL_0:15;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st A1 >= z & z in D1 by A7;
consider a1 being Element of L such that
A15: A1 >= a1 and
A16: a1 in D1 by A14;
x1 >= a1 "\/" b1 by A6,A13,A9,A15,A11,YELLOW_3:3;
then
A17: uparrow (D1 "\/" D2) = {s where s is Element of L: ex z being Element
of L st s >= z & z in D1 "\/" D2} & x >= a1 "\/" b1 by A4,ORDERS_2:3
,WAYBEL_0:15;
a1 "\/" b1 in D1 "\/" D2 by A16,A12;
hence thesis by A2,A17;
end;
theorem
for L being with_suprema Poset, D1, D2 being Subset of L holds uparrow
((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)
proof
let L be with_suprema Poset, D1, D2 be Subset of L;
A1: uparrow (D1 "\/" D2) = {s where s is Element of L: ex z being Element of
L st s >= z & z in D1 "\/" D2} by WAYBEL_0:15;
thus uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) by Th34
;
let q be object;
assume q in uparrow (D1 "\/" D2);
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st s >= z & z in D1 "\/" D2 by A1;
A4: uparrow ((uparrow D1) "\/" (uparrow D2)) = {x where x is Element of L:
ex t being Element of L st x >= t & t in (uparrow D1) "\/" (uparrow D2)} by
WAYBEL_0:15;
A5: D1 is Subset of uparrow D1 & D2 is Subset of uparrow D2 by WAYBEL_0:16;
consider x being Element of L such that
A6: s >= x and
A7: x in D1 "\/" D2 by A3;
ex a, b being Element of L st x = a "\/" b & a in D1 & b in D2 by A7;
then x in (uparrow D1) "\/" (uparrow D2) by A5;
hence thesis by A4,A2,A6;
end;
begin :: The Meet of Subsets
definition
let L be non empty RelStr, D1, D2 be Subset of L;
func D1 "/\" D2 -> Subset of L equals
{ x "/\" y where x, y is Element of L
: x in D1 & y in D2 };
coherence
proof
{ x "/\" y where x, y is Element of L : x in D1 & y in D2 } c= the
carrier of L
proof
let q be object;
assume q in { x "/\" y where x, y is Element of L : x in D1 & y in D2 };
then ex a, b being Element of L st q = a "/\" b & a in D1 & b in D2;
hence thesis;
end;
hence thesis;
end;
end;
definition
let L be with_infima antisymmetric RelStr, D1, D2 be Subset of L;
redefine func D1 "/\" D2; :: redefines "/\" (YELLOW_4, definition)
commutativity
proof
let D1, D2 be Subset of L;
thus D1 "/\" D2 c= D2 "/\" D1
proof
let q be object;
assume q in D1 "/\" D2;
then ex x, y being Element of L st q = x "/\" y & x in D1 & y in D2;
hence thesis;
end;
let q be object;
assume q in D2 "/\" D1;
then ex x, y being Element of L st q = x "/\" y & x in D2 & y in D1;
hence thesis;
end;
end;
theorem
for L being non empty RelStr, X being Subset of L holds X "/\" {}L = {}
proof
let L be non empty RelStr, X be Subset of L;
thus X "/\" {}L c= {}
proof
let a be object;
assume a in X "/\" {}L;
then ex s,t be Element of L st a = s "/\" t & s in X & t in {}L;
hence thesis;
end;
thus thesis;
end;
theorem
for L being non empty RelStr, X, Y being Subset of L, x, y being
Element of L st x in X & y in Y holds x "/\" y in X "/\" Y;
theorem
for L being antisymmetric with_infima RelStr for A being Subset of L,
B being non empty Subset of L holds A is_coarser_than A "/\" B
proof
let L be antisymmetric with_infima RelStr, A be Subset of L, B be non empty
Subset of L;
consider b being object such that
A1: b in B by XBOOLE_0:def 1;
reconsider b as Element of B by A1;
let q be Element of L such that
A2: q in A;
take q "/\" b;
thus q "/\" b in A "/\" B by A2;
thus thesis by YELLOW_0:23;
end;
theorem
for L being antisymmetric with_infima RelStr for A, B being Subset of
L holds A "/\" B is_finer_than A
proof
let L be antisymmetric with_infima RelStr, A, B be Subset of L;
let q be Element of L;
assume q in A "/\" B;
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A and
y in B;
take x;
thus x in A by A2;
thus thesis by A1,YELLOW_0:23;
end;
theorem
for L being antisymmetric reflexive with_infima RelStr for A being
Subset of L holds A c= A "/\" A
proof
let L be antisymmetric reflexive with_infima RelStr, A be Subset of L;
let q be object;
assume
A1: q in A;
then reconsider A1 = A as non empty Subset of L;
reconsider q1 = q as Element of A1 by A1;
q1 = q1 "/\" q1 by YELLOW_0:25;
hence thesis;
end;
theorem
for L being with_infima antisymmetric transitive RelStr for D1, D2, D3
being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
proof
let L be with_infima antisymmetric transitive RelStr, D1, D2, D3 be Subset
of L;
thus (D1 "/\" D2) "/\" D3 c= D1 "/\" (D2 "/\" D3)
proof
let q be object;
assume q in (D1 "/\" D2) "/\" D3;
then consider a1, b1 being Element of L such that
A1: q = a1 "/\" b1 and
A2: a1 in D1 "/\" D2 and
A3: b1 in D3;
consider a11, b11 being Element of L such that
A4: a1 = a11 "/\" b11 and
A5: a11 in D1 and
A6: b11 in D2 by A2;
b11 "/\" b1 in D2 "/\" D3 & q = a11 "/\" (b11 "/\" b1) by A1,A3,A4,A6,
LATTICE3:16;
hence thesis by A5;
end;
let q be object;
assume q in D1 "/\" (D2 "/\" D3);
then consider a1, b1 being Element of L such that
A7: q = a1 "/\" b1 & a1 in D1 and
A8: b1 in D2 "/\" D3;
consider a11, b11 being Element of L such that
A9: b1 = a11 "/\" b11 & a11 in D2 and
A10: b11 in D3 by A8;
a1 "/\" a11 in D1 "/\" D2 & q = a1 "/\" a11 "/\" b11 by A7,A9,LATTICE3:16;
hence thesis by A10;
end;
registration
let L be non empty RelStr, D1, D2 be non empty Subset of L;
cluster D1 "/\" D2 -> non empty;
coherence
proof
consider b being object such that
A1: b in D2 by XBOOLE_0:def 1;
reconsider b as Element of D2 by A1;
consider a being object such that
A2: a in D1 by XBOOLE_0:def 1;
reconsider a as Element of D1 by A2;
a "/\" b in { x "/\" y where x, y is Element of L : x in D1 & y in D2 };
hence thesis;
end;
end;
registration
let L be with_infima transitive antisymmetric RelStr, D1, D2 be directed
Subset of L;
cluster D1 "/\" D2 -> directed;
coherence
proof
let a, b be Element of L;
set X = D1 "/\" D2;
assume that
A1: a in X and
A2: b in X;
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "/\" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: y <= z2 & t <= z2 by A5,A8,WAYBEL_0:def 1;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: x <= z1 & s <= z1 by A4,A7,WAYBEL_0:def 1;
take z = z1 "/\" z2;
thus z in X by A11,A9;
thus thesis by A3,A6,A12,A10,YELLOW_3:2;
end;
end;
registration
let L be with_infima transitive antisymmetric RelStr, D1, D2 be filtered
Subset of L;
cluster D1 "/\" D2 -> filtered;
coherence
proof
let a, b be Element of L;
set X = D1 "/\" D2;
assume that
A1: a in X and
A2: b in X;
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "/\" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: y >= z2 & t >= z2 by A5,A8,WAYBEL_0:def 2;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: x >= z1 & s >= z1 by A4,A7,WAYBEL_0:def 2;
take z = z1 "/\" z2;
thus z in X by A11,A9;
thus thesis by A3,A6,A12,A10,YELLOW_3:2;
end;
end;
registration
let L be Semilattice, D1, D2 be lower Subset of L;
cluster D1 "/\" D2 -> lower;
coherence
proof
set X = D1 "/\" D2;
let a, b be Element of L such that
A1: a in X and
A2: b <= a;
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
A6: ex xx being Element of L st x >= xx & y >= xx & for c being Element of
L st x >= c & y >= c holds xx >= c by LATTICE3:def 11;
then x "/\" y <= x by LATTICE3:def 14;
then b <= x by A2,A3,YELLOW_0:def 2;
then
A7: b in D1 by A4,WAYBEL_0:def 19;
x "/\" y <= y by A6,LATTICE3:def 14;
then b <= y by A2,A3,YELLOW_0:def 2;
then
A8: b in D2 by A5,WAYBEL_0:def 19;
b = b "/\" b by YELLOW_0:25;
hence thesis by A7,A8;
end;
end;
theorem Th42:
for L being non empty RelStr, Y being Subset of L, x being
Element of L holds {x} "/\" Y = {x "/\" y where y is Element of L: y in Y}
proof
let L be non empty RelStr, Y be Subset of L, x be Element of L;
thus {x} "/\" Y c= {x "/\" y where y is Element of L: y in Y}
proof
let q be object;
assume q in {x} "/\" Y;
then consider s, t being Element of L such that
A1: q = s "/\" t and
A2: s in {x} and
A3: t in Y;
s = x by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let q be object;
assume q in {x "/\" y where y is Element of L: y in Y};
then
A4: ex y being Element of L st q = x "/\" y & y in Y;
x in {x} by TARSKI:def 1;
hence thesis by A4;
end;
theorem
for L being non empty RelStr, A, B, C being Subset of L holds A "/\" (
B \/ C) = (A "/\" B) \/ (A "/\" C)
proof
let L be non empty RelStr, A, B, C be Subset of L;
thus A "/\" (B \/ C) c= (A "/\" B) \/ (A "/\" C)
proof
let q be object;
assume q in A "/\" (B \/ C);
then consider a, y being Element of L such that
A1: q = a "/\" y & a in A and
A2: y in B \/ C;
y in B or y in C by A2,XBOOLE_0:def 3;
then q in A "/\" B or q in A "/\" C by A1;
hence thesis by XBOOLE_0:def 3;
end;
let q be object such that
A3: q in (A "/\" B) \/ (A "/\" C);
per cases by A3,XBOOLE_0:def 3;
suppose
q in A "/\" B;
then consider a, b being Element of L such that
A4: q = a "/\" b & a in A and
A5: b in B;
b in B \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
suppose
q in A "/\" C;
then consider a, b being Element of L such that
A6: q = a "/\" b & a in A and
A7: b in C;
b in B \/ C by A7,XBOOLE_0:def 3;
hence thesis by A6;
end;
end;
theorem
for L being antisymmetric reflexive with_infima RelStr for A, B, C
being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
proof
let L be antisymmetric reflexive with_infima RelStr, A, B, C be Subset of L;
let q be object such that
A1: q in A \/ (B "/\" C);
per cases by A1,XBOOLE_0:def 3;
suppose
A2: q in A;
then reconsider q1 = q as Element of L;
A3: q1 = q1 "/\" q1 by YELLOW_0:25;
q1 in A \/ B & q1 in A \/ C by A2,XBOOLE_0:def 3;
hence thesis by A3;
end;
suppose
q in B "/\" C;
then consider b, c being Element of L such that
A4: q = b "/\" c and
A5: b in B & c in C;
b in A \/ B & c in A \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
end;
theorem
for L being antisymmetric with_infima RelStr, A being lower Subset of
L for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
proof
let L be antisymmetric with_infima RelStr, A be lower Subset of L, B, C be
Subset of L;
let q be object;
assume q in (A \/ B) "/\" (A \/ C);
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A \/ B & y in A \/ C;
A3: x "/\" y <= x by YELLOW_0:23;
A4: x "/\" y <= y by YELLOW_0:23;
per cases by A2,XBOOLE_0:def 3;
suppose
x in A & y in A;
then q in A by A1,A3,WAYBEL_0:def 19;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in A & y in C;
then q in A by A1,A3,WAYBEL_0:def 19;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in B & y in A;
then q in A by A1,A4,WAYBEL_0:def 19;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in B & y in C;
then x "/\" y in B "/\" C;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
Lm3: now
let L be non empty RelStr, x, y be Element of L;
thus {a "/\" b where a, b is Element of L : a in {x} & b in {y}} = {x "/\" y
}
proof
thus {a "/\" b where a, b is Element of L : a in {x} & b in {y}} c= {x
"/\" y}
proof
let q be object;
assume q in {a "/\" b where a, b is Element of L : a in {x} & b in {y}};
then consider u,v being Element of L such that
A1: q = u "/\" v and
A2: u in {x} & v in {y};
u = x & v = y by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let q be object;
assume q in {x "/\" y};
then
A3: q = x "/\" y by TARSKI:def 1;
x in {x} & y in {y} by TARSKI:def 1;
hence thesis by A3;
end;
end;
Lm4: now
let L be non empty RelStr, x, y, z be Element of L;
thus {a "/\" b where a, b is Element of L : a in {x} & b in {y,z}} = {x "/\"
y, x "/\" z}
proof
thus {a "/\" b where a, b is Element of L : a in {x} & b in {y,z}} c= {x
"/\" y, x "/\" z}
proof
let q be object;
assume
q in {a "/\" b where a, b is Element of L : a in {x} & b in {y,z }};
then consider u,v being Element of L such that
A1: q = u "/\" v and
A2: u in {x} and
A3: v in {y,z};
A4: v = y or v = z by A3,TARSKI:def 2;
u = x by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let q be object;
A5: z in {y,z} by TARSKI:def 2;
assume q in {x "/\" y, x "/\" z};
then
A6: q = x "/\" y or q = x "/\" z by TARSKI:def 2;
x in {x} & y in {y,z} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
end;
theorem
for L being non empty RelStr, x, y being Element of L holds {x} "/\" {
y} = {x "/\" y} by Lm3;
theorem
for L being non empty RelStr, x, y, z being Element of L holds {x}
"/\" {y,z} = {x "/\" y, x "/\" z} by Lm4;
theorem
for L being non empty RelStr, X1, X2, Y1, Y2 being Subset of L st X1
c= Y1 & X2 c= Y2 holds X1 "/\" X2 c= Y1 "/\" Y2
proof
let L be non empty RelStr, X1, X2, Y1, Y2 be Subset of L such that
A1: X1 c= Y1 & X2 c= Y2;
let q be object;
assume q in X1 "/\" X2;
then ex x, y being Element of L st q = x "/\" y & x in X1 & y in X2;
hence thesis by A1;
end;
theorem Th49:
for L being antisymmetric reflexive with_infima RelStr for A, B
being Subset of L holds A /\ B c= A "/\" B
proof
let L be antisymmetric reflexive with_infima RelStr, A, B be Subset of L;
let q be object;
assume
A1: q in A /\ B;
then reconsider A1 = A as non empty Subset of L;
reconsider q1 = q as Element of A1 by A1,XBOOLE_0:def 4;
A2: q1 = q1 "/\" q1 by YELLOW_0:25;
q in B by A1,XBOOLE_0:def 4;
hence thesis by A2;
end;
theorem Th50:
for L being antisymmetric reflexive with_infima RelStr for A, B
being lower Subset of L holds A "/\" B = A /\ B
proof
let L be antisymmetric reflexive with_infima RelStr, A, B be lower Subset of
L;
thus A "/\" B c= A /\ B
proof
let q be object;
assume q in A "/\" B;
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A and
A3: y in B;
A4: ex z being Element of L st x >= z & y >= z & for c being Element of L
st x >= c & y >= c holds z >= c by LATTICE3:def 11;
then x "/\" y <= y by LATTICE3:def 14;
then
A5: q in B by A1,A3,WAYBEL_0:def 19;
x "/\" y <= x by A4,LATTICE3:def 14;
then q in A by A1,A2,WAYBEL_0:def 19;
hence thesis by A5,XBOOLE_0:def 4;
end;
thus thesis by Th49;
end;
theorem
for L being with_infima reflexive antisymmetric RelStr for D being
Subset of L, x being Element of L st x is_>=_than D holds {x} "/\" D = D
proof
let L be with_infima reflexive antisymmetric RelStr, D be Subset of L, x be
Element of L such that
A1: x is_>=_than D;
A2: {x} "/\" D = { x "/\" y where y is Element of L : y in D } by Th42;
thus {x} "/\" D c= D
proof
let q be object;
assume q in {x} "/\" D;
then consider y being Element of L such that
A3: q = x "/\" y and
A4: y in D by A2;
x >= y by A1,A4;
hence thesis by A3,A4,YELLOW_0:25;
end;
let q be object;
assume
A5: q in D;
then reconsider D1 = D as non empty Subset of L;
reconsider y = q as Element of D1 by A5;
x >= y by A1;
then q = x "/\" y by YELLOW_0:25;
hence thesis by A2;
end;
theorem
for L being with_infima antisymmetric RelStr for D being Subset of L,
x being Element of L holds {x} "/\" D is_<=_than x
proof
let L be with_infima antisymmetric RelStr, D be Subset of L, x be Element of
L;
let b be Element of L;
A1: {x} "/\" D = { x "/\" h where h is Element of L : h in D } by Th42;
assume b in {x} "/\" D;
then consider h being Element of L such that
A2: b = x "/\" h and
h in D by A1;
ex w being Element of L st x >= w & h >= w & for c being Element of L st
x >= c & h >= c holds w >= c by LATTICE3:def 11;
hence thesis by A2,LATTICE3:def 14;
end;
theorem
for L being Semilattice, X being Subset of L, x being Element of L st
ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds sup ({x} "/\" X) <= x "/\" sup X
proof
let L be Semilattice, X be Subset of L, x be Element of L such that
A1: ex_sup_of {x} "/\" X,L and
A2: ex_sup_of X,L;
A3: {x} "/\" X = {x "/\" y where y is Element of L : y in X} by Th42;
{x} "/\" X is_<=_than x "/\" sup X
proof
let q be Element of L;
assume q in {x} "/\" X;
then consider y being Element of L such that
A4: q = x "/\" y and
A5: y in X by A3;
x <= x & y <= sup X by A2,A5,Th1;
hence q <= x "/\" sup X by A4,YELLOW_3:2;
end;
hence thesis by A1,YELLOW_0:def 9;
end;
theorem Th54:
for L being complete transitive antisymmetric non empty RelStr
for A being Subset of L, B being non empty Subset of L holds A is_>=_than inf (
A "/\" B)
proof
let L be complete transitive antisymmetric non empty RelStr, A be Subset
of L, B be non empty Subset of L;
set b = the Element of B;
let x be Element of L;
assume x in A;
then
A1: x "/\" b in A "/\" B;
ex xx being Element of L st x >= xx & b >= xx & for c being Element of L
st x >= c & b >= c holds xx >= c by LATTICE3:def 11;
then
A2: x >= x "/\" b by LATTICE3:def 14;
ex_inf_of A "/\" B,L by YELLOW_0:17;
then A "/\" B is_>=_than inf (A "/\" B) by YELLOW_0:def 10;
then x "/\" b >= inf (A "/\" B) by A1;
hence thesis by A2,YELLOW_0:def 2;
end;
theorem Th55:
for L being with_infima transitive antisymmetric RelStr for a, b
being Element of L, A, B being Subset of L st a is_<=_than A & b is_<=_than B
holds a "/\" b is_<=_than A "/\" B
proof
let L be with_infima transitive antisymmetric RelStr, a, b be Element of L,
A, B be Subset of L such that
A1: a is_<=_than A & b is_<=_than B;
let q be Element of L;
assume q in A "/\" B;
then consider x, y being Element of L such that
A2: q = x "/\" y and
A3: x in A & y in B;
a <= x & b <= y by A1,A3;
hence thesis by A2,YELLOW_3:2;
end;
theorem
for L being with_infima transitive antisymmetric RelStr for a, b being
Element of L, A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a
"/\" b is_>=_than A "/\" B
proof
let L be with_infima transitive antisymmetric RelStr, a, b be Element of L,
A, B be Subset of L such that
A1: a is_>=_than A & b is_>=_than B;
let q be Element of L;
assume q in A "/\" B;
then consider x, y being Element of L such that
A2: q = x "/\" y and
A3: x in A & y in B;
a >= x & b >= y by A1,A3;
hence thesis by A2,YELLOW_3:2;
end;
theorem
for L being complete non empty Poset for A, B being non empty Subset
of L holds inf (A "/\" B) = inf A "/\" inf B
proof
let L be complete non empty Poset, A, B be non empty Subset of L;
B is_>=_than inf (A "/\" B) by Th54;
then
A1: inf B >= inf (A "/\" B) by YELLOW_0:33;
A is_>=_than inf (A "/\" B) by Th54;
then inf A >= inf (A "/\" B) by YELLOW_0:33;
then
A2: inf A "/\" inf B >= inf (A "/\" B) "/\" inf (A "/\" B) by A1,YELLOW_3:2;
A is_>=_than inf A & B is_>=_than inf B by YELLOW_0:33;
then ex_inf_of A "/\" B,L & A "/\" B is_>=_than inf A "/\" inf B by Th55,
YELLOW_0:17;
then
A3: inf (A "/\" B) >= inf A "/\" inf B by YELLOW_0:def 10;
inf (A "/\" B) "/\" inf (A "/\" B) = inf (A "/\" B) by YELLOW_0:25;
hence thesis by A3,A2,ORDERS_2:2;
end;
theorem
for L being Semilattice, x, y being Element of InclPoset Ids L for x1,
y1 being Subset of L st x = x1 & y = y1 holds x "/\" y = x1 "/\" y1
proof
let L be Semilattice, x, y be Element of InclPoset Ids L, x1, y1 be Subset
of L;
assume
A1: x = x1 & y = y1;
then
A2: x1 is lower & y1 is lower by YELLOW_2:41;
thus x "/\" y = x /\ y by YELLOW_2:43
.= x1 "/\" y1 by A1,A2,Th50;
end;
theorem
for L being with_infima antisymmetric RelStr for X being Subset of L,
Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
proof
let L be with_infima antisymmetric RelStr, X be Subset of L, Y be non empty
Subset of L;
consider y being object such that
A1: y in Y by XBOOLE_0:def 1;
reconsider y as Element of Y by A1;
let q be object;
assume
A2: q in X;
then reconsider X1 = X as non empty Subset of L;
reconsider x = q as Element of X1 by A2;
ex s being Element of L st x >= s & y >= s & for c being Element of L st
x >= c & y >= c holds s >= c by LATTICE3:def 11;
then
A3: x "/\" y <= x by LATTICE3:def 14;
uparrow (X "/\" Y) = {s where s is Element of L: ex y being Element of L
st s >= y & y in X "/\" Y} & x "/\" y in X1 "/\" Y by WAYBEL_0:15;
hence thesis by A3;
end;
theorem
for L being non empty RelStr, D being Subset of [:L,L:] holds union {X
where X is Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in
proj1 D} = proj1 D "/\" proj2 D
proof
let L be non empty RelStr, D be Subset of [:L,L:];
set D1 = proj1 D, D2 = proj2 D;
defpred P[set] means ex x being Element of L st $1 = {x} "/\" proj2 D & x in
proj1 D;
thus union {X where X is Subset of L: P[X]} c= D1 "/\" D2
proof
let q be object;
assume q in union {X where X is Subset of L: P[X]};
then consider w being set such that
A1: q in w and
A2: w in {X where X is Subset of L: P[X]} by TARSKI:def 4;
consider e being Subset of L such that
A3: w = e and
A4: P[e] by A2;
consider p being Element of L such that
A5: e = {p} "/\" D2 and
A6: p in D1 by A4;
{p} "/\" D2 = { p "/\" y where y is Element of L : y in D2 } by Th42;
then ex y being Element of L st q = p "/\" y & y in D2 by A1,A3,A5;
hence thesis by A6;
end;
let q be object;
assume q in D1 "/\" D2;
then consider x, y being Element of L such that
A7: q = x "/\" y and
A8: x in D1 and
A9: y in D2;
{x} "/\" D2 = { x "/\" d where d is Element of L : d in D2 } by Th42;
then
A10: q in {x} "/\" D2 by A7,A9;
{x} "/\" D2 in {X where X is Subset of L: P[X]} by A8;
hence thesis by A10,TARSKI:def 4;
end;
theorem Th61:
for L being transitive antisymmetric with_infima RelStr for D1,
D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c=
downarrow (D1 "/\" D2)
proof
let L be transitive antisymmetric with_infima RelStr, D1, D2 be Subset of L;
A1: downarrow ((downarrow D1) "/\" (downarrow D2)) = {x where x is Element
of L: ex t being Element of L st x <= t & t in (downarrow D1) "/\" (downarrow
D2)} by WAYBEL_0:14;
let y be object;
assume y in downarrow ((downarrow D1) "/\" (downarrow D2));
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st x <= t & t in (downarrow D1) "/\" (
downarrow D2) by A1;
consider x1 being Element of L such that
A4: x <= x1 and
A5: x1 in (downarrow D1) "/\" (downarrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "/\" b and
A7: a in downarrow D1 and
A8: b in downarrow D2 by A5;
downarrow D2 = {s2 where s2 is Element of L: ex z being Element of L st
s2 <= z & z in D2} by WAYBEL_0:14;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st B1 <= z & z in D2 by A8;
consider b1 being Element of L such that
A11: B1 <= b1 and
A12: b1 in D2 by A10;
downarrow D1 = {s1 where s1 is Element of L: ex z being Element of L st
s1 <= z & z in D1} by WAYBEL_0:14;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st A1 <= z & z in D1 by A7;
consider a1 being Element of L such that
A15: A1 <= a1 and
A16: a1 in D1 by A14;
x1 <= a1 "/\" b1 by A6,A13,A9,A15,A11,YELLOW_3:2;
then
A17: downarrow (D1 "/\" D2) = {s where s is Element of L: ex z being Element
of L st s <= z & z in D1 "/\" D2} & x <= a1 "/\" b1 by A4,ORDERS_2:3
,WAYBEL_0:14;
a1 "/\" b1 in D1 "/\" D2 by A16,A12;
hence thesis by A2,A17;
end;
theorem
for L being Semilattice, D1, D2 being Subset of L holds downarrow ((
downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)
proof
let L be Semilattice, D1, D2 be Subset of L;
A1: downarrow (D1 "/\" D2) = {s where s is Element of L: ex z being Element
of L st s <= z & z in D1 "/\" D2} by WAYBEL_0:14;
thus downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2
) by Th61;
let q be object;
assume q in downarrow (D1 "/\" D2);
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st s <= z & z in D1 "/\" D2 by A1;
A4: downarrow ((downarrow D1) "/\" (downarrow D2)) = {x where x is Element
of L: ex t being Element of L st x <= t & t in (downarrow D1) "/\" (downarrow
D2)} by WAYBEL_0:14;
A5: D1 is Subset of downarrow D1 & D2 is Subset of downarrow D2 by WAYBEL_0:16;
consider x being Element of L such that
A6: s <= x and
A7: x in D1 "/\" D2 by A3;
ex a, b being Element of L st x = a "/\" b & a in D1 & b in D2 by A7;
then x in (downarrow D1) "/\" (downarrow D2) by A5;
hence thesis by A4,A2,A6;
end;
theorem Th63:
for L being transitive antisymmetric with_infima RelStr for D1,
D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow
(D1 "/\" D2)
proof
let L be transitive antisymmetric with_infima RelStr, D1, D2 be Subset of L;
A1: uparrow ((uparrow D1) "/\" (uparrow D2)) = {x where x is Element of L:
ex t being Element of L st x >= t & t in (uparrow D1) "/\" (uparrow D2)} by
WAYBEL_0:15;
let y be object;
assume y in uparrow ((uparrow D1) "/\" (uparrow D2));
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st x >= t & t in (uparrow D1) "/\" (uparrow
D2) by A1;
consider x1 being Element of L such that
A4: x >= x1 and
A5: x1 in (uparrow D1) "/\" (uparrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "/\" b and
A7: a in uparrow D1 and
A8: b in uparrow D2 by A5;
uparrow D2 = {s2 where s2 is Element of L: ex z being Element of L st s2
>= z & z in D2} by WAYBEL_0:15;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st B1 >= z & z in D2 by A8;
consider b1 being Element of L such that
A11: B1 >= b1 and
A12: b1 in D2 by A10;
uparrow D1 = {s1 where s1 is Element of L: ex z being Element of L st s1
>= z & z in D1} by WAYBEL_0:15;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st A1 >= z & z in D1 by A7;
consider a1 being Element of L such that
A15: A1 >= a1 and
A16: a1 in D1 by A14;
x1 >= a1 "/\" b1 by A6,A13,A9,A15,A11,YELLOW_3:2;
then
A17: uparrow (D1 "/\" D2) = {s where s is Element of L: ex z being Element
of L st s >= z & z in D1 "/\" D2} & x >= a1 "/\" b1 by A4,ORDERS_2:3
,WAYBEL_0:15;
a1 "/\" b1 in D1 "/\" D2 by A16,A12;
hence thesis by A2,A17;
end;
theorem
for L being Semilattice, D1, D2 being Subset of L holds uparrow ((
uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)
proof
let L be Semilattice, D1, D2 be Subset of L;
A1: uparrow (D1 "/\" D2) = {s where s is Element of L: ex z being Element of
L st s >= z & z in D1 "/\" D2} by WAYBEL_0:15;
thus uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) by Th63
;
let q be object;
assume q in uparrow (D1 "/\" D2);
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st s >= z & z in D1 "/\" D2 by A1;
A4: uparrow ((uparrow D1) "/\" (uparrow D2)) = {x where x is Element of L:
ex t being Element of L st x >= t & t in (uparrow D1) "/\" (uparrow D2)} by
WAYBEL_0:15;
A5: D1 is Subset of uparrow D1 & D2 is Subset of uparrow D2 by WAYBEL_0:16;
consider x being Element of L such that
A6: s >= x and
A7: x in D1 "/\" D2 by A3;
ex a, b being Element of L st x = a "/\" b & a in D1 & b in D2 by A7;
then x in (uparrow D1) "/\" (uparrow D2) by A5;
hence thesis by A4,A2,A6;
end;