:: 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);