:: Definitions and Properties of the Join and Meet of Subsets
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996-2021 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;
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);
registration
let L be non empty RelStr, D1, D2 be non empty Subset of L;
cluster D1 "\/" D2 -> non empty;
end;
registration
let L be with_suprema transitive antisymmetric RelStr, D1, D2 be directed
Subset of L;
cluster D1 "\/" D2 -> directed;
end;
registration
let L be with_suprema transitive antisymmetric RelStr, D1, D2 be filtered
Subset of L;
cluster D1 "\/" D2 -> filtered;
end;
registration
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);
registration
let L be non empty RelStr, D1, D2 be non empty Subset of L;
cluster D1 "/\" D2 -> non empty;
end;
registration
let L be with_infima transitive antisymmetric RelStr, D1, D2 be directed
Subset of L;
cluster D1 "/\" D2 -> directed;
end;
registration
let L be with_infima transitive antisymmetric RelStr, D1, D2 be filtered
Subset of L;
cluster D1 "/\" D2 -> filtered;
end;
registration
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);