Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Definitions and Properties of the Join and Meet of Subsets

by
Artur Kornilowicz

MML identifier: YELLOW_4
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDERS_1, YELLOW_0, LATTICES, LATTICE3, SETFAM_1, RELAT_2, BOOLE,
WAYBEL_0, QUANTAL1, ORDINAL2, BHSP_3, YELLOW_1, TARSKI, FUNCT_5;
notation TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, LATTICE3, YELLOW_0, STRUCT_0,
ORDERS_1, YELLOW_1, WAYBEL_0, YELLOW_3;
constructors YELLOW_2, YELLOW_3, LATTICE3, MEMBERED, PRE_TOPC;
clusters STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, SUBSET_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Preliminaries

theorem :: YELLOW_4:1
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);

theorem :: YELLOW_4:2
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;

definition let L be RelStr,
A, B be Subset of L;
pred A is_finer_than B means
:: YELLOW_4:def 1
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
:: YELLOW_4:def 2
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;
reflexivity;
redefine pred B is_coarser_than A;
reflexivity;
end;

theorem :: YELLOW_4:3
for L being RelStr, B being Subset of L holds {}L is_finer_than B;

theorem :: YELLOW_4:4
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;

theorem :: YELLOW_4:5
for L being RelStr, A, B being Subset of L st B is_finer_than A & A is lower
holds B c= A;

theorem :: YELLOW_4:6
for L being RelStr, A being Subset of L holds {}L is_coarser_than A;

theorem :: YELLOW_4:7
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;

theorem :: YELLOW_4:8
for L being RelStr, A, B being Subset of L st A is_coarser_than B & B is
upper
holds A c= B;

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
:: YELLOW_4:def 3
{ x "\/" y where x, y is Element of L : x in D1 & y in D2 };
end;

definition let L be with_suprema antisymmetric RelStr,
D1, D2 be Subset of L;
redefine func D1 "\/" D2;
commutativity;
end;

theorem :: YELLOW_4:9
for L being non empty RelStr, X being Subset of L holds X "\/" {}L = {};

theorem :: YELLOW_4:10
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 :: YELLOW_4:11
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;

theorem :: YELLOW_4:12
for L being antisymmetric with_suprema RelStr, A, B being Subset of L
holds A "\/" B is_coarser_than A;

theorem :: YELLOW_4:13
for L being antisymmetric reflexive with_suprema RelStr
for A being Subset of L holds A c= A "\/" A;

theorem :: YELLOW_4:14
for L being with_suprema antisymmetric transitive RelStr
for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/"
D3);

definition let L be non empty RelStr,
D1, D2 be non empty Subset of L;
cluster D1 "\/" D2 -> non empty;
end;

definition let L be with_suprema transitive antisymmetric RelStr,
D1, D2 be directed Subset of L;
cluster D1 "\/" D2 -> directed;
end;

definition let L be with_suprema transitive antisymmetric RelStr,
D1, D2 be filtered Subset of L;
cluster D1 "\/" D2 -> filtered;
end;

definition let L be with_suprema Poset,
D1, D2 be upper Subset of L;
cluster D1 "\/" D2 -> upper;
end;

theorem :: YELLOW_4:15
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};

theorem :: YELLOW_4:16
for L being non empty RelStr, A, B, C being Subset of L
holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C);

theorem :: YELLOW_4:17
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);

theorem :: YELLOW_4:18
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);

theorem :: YELLOW_4:19
for L being non empty RelStr, x, y being Element of L
holds {x} "\/" {y} = {x "\/" y};

theorem :: YELLOW_4:20
for L being non empty RelStr, x, y, z being Element of L
holds {x} "\/" {y,z} = {x "\/" y, x "\/" z};

theorem :: YELLOW_4:21
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;

theorem :: YELLOW_4:22
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;

theorem :: YELLOW_4:23
for L being with_suprema antisymmetric RelStr
for D being Subset of L, x being Element of L
holds x is_<=_than {x} "\/" D;

theorem :: YELLOW_4:24
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);

theorem :: YELLOW_4:25
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);

theorem :: YELLOW_4:26
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;

theorem :: YELLOW_4:27
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;

theorem :: YELLOW_4:28
for L being complete (non empty Poset)
for A, B being non empty Subset of L holds sup (A "\/" B) = sup A "\/" sup B;

theorem :: YELLOW_4:29
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);

theorem :: YELLOW_4:30
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);

theorem :: YELLOW_4:31
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;

theorem :: YELLOW_4:32
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);

theorem :: YELLOW_4:33
for L being with_suprema Poset, D1, D2 being Subset of L holds
downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2);

theorem :: YELLOW_4:34
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);

theorem :: YELLOW_4:35
for L being with_suprema Poset, D1, D2 being Subset of L holds
uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2);

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
:: YELLOW_4:def 4
{ x "/\" y where x, y is Element of L : x in D1 & y in D2 };
end;

definition let L be with_infima antisymmetric RelStr,
D1, D2 be Subset of L;
redefine func D1 "/\" D2;
commutativity;
end;

theorem :: YELLOW_4:36
for L being non empty RelStr, X being Subset of L holds X "/\" {}L = {};

theorem :: YELLOW_4:37
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 :: YELLOW_4:38
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;

theorem :: YELLOW_4:39
for L being antisymmetric with_infima RelStr
for A, B being Subset of L holds A "/\" B is_finer_than A;

theorem :: YELLOW_4:40
for L being antisymmetric reflexive with_infima RelStr
for A being Subset of L holds A c= A "/\" A;

theorem :: YELLOW_4:41
for L being with_infima antisymmetric transitive RelStr
for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\"
D3);

definition let L be non empty RelStr,
D1, D2 be non empty Subset of L;
cluster D1 "/\" D2 -> non empty;
end;

definition let L be with_infima transitive antisymmetric RelStr,
D1, D2 be directed Subset of L;
cluster D1 "/\" D2 -> directed;
end;

definition let L be with_infima transitive antisymmetric RelStr,
D1, D2 be filtered Subset of L;
cluster D1 "/\" D2 -> filtered;
end;

definition let L be Semilattice,
D1, D2 be lower Subset of L;
cluster D1 "/\" D2 -> lower;
end;

theorem :: YELLOW_4:42
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};

theorem :: YELLOW_4:43
for L being non empty RelStr, A, B, C being Subset of L
holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C);

theorem :: YELLOW_4:44
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);

theorem :: YELLOW_4:45
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);

theorem :: YELLOW_4:46
for L being non empty RelStr, x, y being Element of L
holds {x} "/\" {y} = {x "/\" y};

theorem :: YELLOW_4:47
for L being non empty RelStr, x, y, z being Element of L
holds {x} "/\" {y,z} = {x "/\" y, x "/\" z};

theorem :: YELLOW_4:48
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;

theorem :: YELLOW_4:49
for L being antisymmetric reflexive with_infima RelStr
for A, B being Subset of L holds A /\ B c= A "/\" B;

theorem :: YELLOW_4:50
for L being antisymmetric reflexive with_infima RelStr
for A, B being lower Subset of L holds A "/\" B = A /\ B;

theorem :: YELLOW_4:51
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;

theorem :: YELLOW_4:52
for L being with_infima antisymmetric RelStr
for D being Subset of L, x being Element of L
holds {x} "/\" D is_<=_than x;

theorem :: YELLOW_4:53
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;

theorem :: YELLOW_4:54
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);

theorem :: YELLOW_4:55
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;

theorem :: YELLOW_4:56
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;

theorem :: YELLOW_4:57
for L being complete (non empty Poset)
for A, B being non empty Subset of L holds inf (A "/\" B) = inf A "/\" inf B;

theorem :: YELLOW_4:58
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;

theorem :: YELLOW_4:59
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);

theorem :: YELLOW_4:60
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;

theorem :: YELLOW_4:61
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);

theorem :: YELLOW_4:62
for L being Semilattice, D1, D2 being Subset of L holds
downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2);

theorem :: YELLOW_4:63
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);

theorem :: YELLOW_4:64
for L being Semilattice, D1, D2 being Subset of L holds
uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2);

```