:: Families of Sets :: by Beata Padlewska :: :: Received April 5, 1989 :: Copyright (c) 1990-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 XBOOLE_0, TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1; constructors TARSKI, ENUMSET1, SUBSET_1; registrations XBOOLE_0, SUBSET_1; requirements SUBSET, BOOLE; begin reserve X,Y,Z,Z1,Z2,D for set,x,y for object; definition let X; func meet X -> set means :: SETFAM_1:def 1 for x being object holds x in it iff for Y holds Y in X implies x in Y if X <> {} otherwise it = {}; end; :: Intersection of families of sets theorem :: SETFAM_1:1 meet {} = {}; theorem :: SETFAM_1:2 meet X c= union X; theorem :: SETFAM_1:3 Z in X implies meet X c= Z; theorem :: SETFAM_1:4 {} in X implies meet X = {}; theorem :: SETFAM_1:5 X <> {} & (for Z1 st Z1 in X holds Z c= Z1) implies Z c= meet X; theorem :: SETFAM_1:6 X <> {} & X c= Y implies meet Y c= meet X; theorem :: SETFAM_1:7 X in Y & X c= Z implies meet Y c= Z; theorem :: SETFAM_1:8 X in Y & X misses Z implies meet Y misses Z; theorem :: SETFAM_1:9 X <> {} & Y <> {} implies meet (X \/ Y) = meet X /\ meet Y; theorem :: SETFAM_1:10 meet {X} = X; theorem :: SETFAM_1:11 meet {X,Y} = X /\ Y; reserve SFX,SFY,SFZ for set; definition let SFX,SFY; pred SFX is_finer_than SFY means :: SETFAM_1:def 2 for X st X in SFX ex Y st Y in SFY & X c= Y; reflexivity; pred SFY is_coarser_than SFX means :: SETFAM_1:def 3 for Y st Y in SFY ex X st X in SFX & X c= Y; reflexivity; end; theorem :: SETFAM_1:12 SFX c= SFY implies SFX is_finer_than SFY; theorem :: SETFAM_1:13 SFX is_finer_than SFY implies union SFX c= union SFY; theorem :: SETFAM_1:14 SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY; theorem :: SETFAM_1:15 {} is_finer_than SFX; theorem :: SETFAM_1:16 SFX is_finer_than {} implies SFX = {}; theorem :: SETFAM_1:17 SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ; theorem :: SETFAM_1:18 SFX is_finer_than {Y} implies for X st X in SFX holds X c= Y; theorem :: SETFAM_1:19 SFX is_finer_than {X,Y} implies for Z st Z in SFX holds Z c= X or Z c= Y; definition let SFX,SFY; func UNION (SFX,SFY) -> set means :: SETFAM_1:def 4 Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y; commutativity; func INTERSECTION (SFX,SFY) -> set means :: SETFAM_1:def 5 Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y; commutativity; func DIFFERENCE (SFX,SFY) -> set means :: SETFAM_1:def 6 Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y; end; theorem :: SETFAM_1:20 SFX is_finer_than UNION(SFX,SFX); theorem :: SETFAM_1:21 INTERSECTION(SFX,SFX) is_finer_than SFX; theorem :: SETFAM_1:22 DIFFERENCE(SFX,SFX) is_finer_than SFX; theorem :: SETFAM_1:23 SFX meets SFY implies meet SFX /\ meet SFY = meet INTERSECTION(SFX,SFY ); theorem :: SETFAM_1:24 SFY <> {} implies X \/ meet SFY = meet UNION({X},SFY); theorem :: SETFAM_1:25 X /\ union SFY = union INTERSECTION({X},SFY); theorem :: SETFAM_1:26 SFY <> {} implies X \ union SFY = meet DIFFERENCE({X},SFY); theorem :: SETFAM_1:27 SFY <> {} implies X \ meet SFY = union DIFFERENCE ({X},SFY); theorem :: SETFAM_1:28 union INTERSECTION (SFX,SFY) = union SFX /\ union SFY; theorem :: SETFAM_1:29 SFX <> {} & SFY <> {} implies meet SFX \/ meet SFY c= meet UNION (SFX, SFY); theorem :: SETFAM_1:30 meet DIFFERENCE (SFX,SFY) c= meet SFX \ meet SFY; :: Family of subsets of a set definition let D be set; mode Subset-Family of D is Subset of bool D; end; reserve F,G for Subset-Family of D; reserve P for Subset of D; definition let D,F; redefine func union F -> Subset of D; end; definition let D,F; redefine func meet F -> Subset of D; end; theorem :: SETFAM_1:31 (for P holds P in F iff P in G) implies F=G; definition let D,F; func COMPLEMENT(F) -> Subset-Family of D means :: SETFAM_1:def 7 for P being Subset of D holds P in it iff P` in F; involutiveness; end; theorem :: SETFAM_1:32 F <> {} implies COMPLEMENT(F) <> {}; theorem :: SETFAM_1:33 F <> {} implies [#] D \ union F = meet (COMPLEMENT(F)); theorem :: SETFAM_1:34 F <> {} implies union COMPLEMENT(F) = [#] D \ meet F; begin :: Addendum :: from YELLOW_8, 2004.07.25 theorem :: SETFAM_1:35 for X being set, F being Subset-Family of X for P being Subset of X holds P` in COMPLEMENT F iff P in F; theorem :: SETFAM_1:36 for X being set, F,G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds F c= G; theorem :: SETFAM_1:37 for X being set, F,G being Subset-Family of X holds COMPLEMENT F c= G iff F c= COMPLEMENT G; theorem :: SETFAM_1:38 for X being set, F,G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds F = G; theorem :: SETFAM_1:39 for X being set, F,G being Subset-Family of X holds COMPLEMENT(F \/ G) = COMPLEMENT F \/ COMPLEMENT G; theorem :: SETFAM_1:40 for X being set, F being Subset-Family of X st F = {X} holds COMPLEMENT F = {{}}; registration let X be set, F be empty Subset-Family of X; cluster COMPLEMENT F -> empty; end; :: from AMI_1 definition let IT be set; attr IT is with_non-empty_elements means :: SETFAM_1:def 8 not {} in IT; end; registration cluster non empty with_non-empty_elements for set; end; registration let A be non empty set; cluster { A } -> with_non-empty_elements; let B be non empty set; cluster { A, B } -> with_non-empty_elements; let C be non empty set; cluster { A, B, C } -> with_non-empty_elements; let D be non empty set; cluster { A, B, C, D } -> with_non-empty_elements; let E be non empty set; cluster { A, B, C, D, E } -> with_non-empty_elements; let F be non empty set; cluster { A, B, C, D, E, F } -> with_non-empty_elements; let G be non empty set; cluster { A, B, C, D, E, F, G } -> with_non-empty_elements; let H be non empty set; cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements; let I be non empty set; cluster { A, B, C, D, E, F, G, H, I } -> with_non-empty_elements; let J be non empty set; cluster { A, B, C, D, E, F, G, H, I, J } -> with_non-empty_elements; end; registration let A,B be with_non-empty_elements set; cluster A \/ B -> with_non-empty_elements; end; :: from LATTICE4 theorem :: SETFAM_1:41 union Y c= Z & X in Y implies X c= Z; :: from LOPCLSET theorem :: SETFAM_1:42 for A,B,X being set holds ( X c= union (A \/ B) & for Y being set st Y in B holds Y misses X ) implies X c= union A; :: from CANTOR_1 definition let M be set; let B be Subset-Family of M; func Intersect B -> Subset of M equals :: SETFAM_1:def 9 meet B if B <> {} otherwise M; end; theorem :: SETFAM_1:43 for X, x being set, R being Subset-Family of X st x in X holds x in Intersect R iff for Y being set st Y in R holds x in Y; theorem :: SETFAM_1:44 for X being set for H, J being Subset-Family of X st H c= J holds Intersect J c= Intersect H; :: from PUA2MSS1, 2005.08.22, A.T registration let X be non empty with_non-empty_elements set; cluster -> non empty for Element of X; end; :: from ABIAN, 2005.08.22, A.T reserve E for set; definition let E; attr E is empty-membered means :: SETFAM_1:def 10 not ex x being non empty set st x in E; end; notation let E; antonym E is with_non-empty_element for E is empty-membered; end; registration cluster with_non-empty_element for set; end; registration cluster with_non-empty_element -> non empty for set; end; :: from TRIANG_1, 2005.08.22 registration let X be with_non-empty_element set; cluster non empty for Element of X; end; :: from MSAFREE1, 2007.03.09, A.T. registration let D be non empty with_non-empty_elements set; cluster union D -> non empty; end; :: missing, 2007.03.09, A.T. registration cluster non empty with_non-empty_elements -> with_non-empty_element for set; end; :: the concept of a cover, 2008.03.08, A.T. definition let X be set; mode Cover of X -> set means :: SETFAM_1:def 11 X c= union it; end; theorem :: SETFAM_1:45 for X being set, F being Subset-Family of X holds F is Cover of X iff union F = X; :: from MEASURE1, 2008.06.08, A.T. theorem :: SETFAM_1:46 {{}} is Subset-Family of X; :: from BORSUK_5 (generalized), 2008.06.08, A.T. definition let X be set; let F be Subset-Family of X; attr F is with_proper_subsets means :: SETFAM_1:def 12 not X in F; end; theorem :: SETFAM_1:47 for TS being set, F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds G is with_proper_subsets; registration let TS be non empty set; cluster with_proper_subsets for Subset-Family of TS; end; theorem :: SETFAM_1:48 for TS being non empty set, A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets; :: from YELLOW21, 2008.09.10, A.T. registration cluster non trivial -> with_non-empty_element for set; end; :: from PCOMPS_1, 2010.02.26, A.T. definition let X be set; redefine func bool X -> Subset-Family of X; end; :: from HAHNBAN, 2011.04.26., A.T. theorem :: SETFAM_1:49 for A being non empty set, b being object st A <> {b} ex a being Element of A st a <> b;