Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Families of Sets

**by****Beata Padlewska**- Received April 5, 1989
- MML identifier: SETFAM_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, TARSKI, SUBSET_1, SETFAM_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1; constructors TARSKI, SUBSET_1, XBOOLE_0; clusters SUBSET_1, XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; begin reserve X,Y,Z,Z1,Z2,D, x,y for set; definition let X; func meet X means :: SETFAM_1:def 1 for x 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 :: canceled; theorem :: SETFAM_1:2 meet {} = {}; theorem :: SETFAM_1:3 meet X c= union X; theorem :: SETFAM_1:4 Z in X implies meet X c= Z; theorem :: SETFAM_1:5 {} in X implies meet X = {}; theorem :: SETFAM_1:6 X <> {} & (for Z1 st Z1 in X holds Z c= Z1) implies Z c= meet X; theorem :: SETFAM_1:7 X <> {} & X c= Y implies meet Y c= meet X; theorem :: SETFAM_1:8 X in Y & X c= Z implies meet Y c= Z; theorem :: SETFAM_1:9 X in Y & X misses Z implies meet Y misses Z; theorem :: SETFAM_1:10 X <> {} & Y <> {} implies meet (X \/ Y) = meet X /\ meet Y; theorem :: SETFAM_1:11 meet {x} = x; theorem :: SETFAM_1:12 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; canceled 4; theorem :: SETFAM_1:17 SFX c= SFY implies SFX is_finer_than SFY; theorem :: SETFAM_1:18 SFX is_finer_than SFY implies union SFX c= union SFY; theorem :: SETFAM_1:19 SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY; theorem :: SETFAM_1:20 {} is_finer_than SFX; theorem :: SETFAM_1:21 SFX is_finer_than {} implies SFX = {}; canceled; theorem :: SETFAM_1:23 SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ; theorem :: SETFAM_1:24 SFX is_finer_than {Y} implies for X st X in SFX holds X c= Y; theorem :: SETFAM_1:25 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) 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) 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) means :: SETFAM_1:def 6 Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y; end; canceled 3; theorem :: SETFAM_1:29 SFX is_finer_than UNION(SFX,SFX); theorem :: SETFAM_1:30 INTERSECTION(SFX,SFX) is_finer_than SFX; theorem :: SETFAM_1:31 DIFFERENCE(SFX,SFX) is_finer_than SFX; canceled 2; theorem :: SETFAM_1:34 SFX meets SFY implies meet SFX /\ meet SFY = meet INTERSECTION(SFX,SFY); theorem :: SETFAM_1:35 SFY <> {} implies X \/ meet SFY = meet UNION({X},SFY); theorem :: SETFAM_1:36 X /\ union SFY = union INTERSECTION({X},SFY); theorem :: SETFAM_1:37 SFY <> {} implies X \ union SFY = meet DIFFERENCE({X},SFY); theorem :: SETFAM_1:38 SFY <> {} implies X \ meet SFY = union DIFFERENCE({X},SFY); theorem :: SETFAM_1:39 union INTERSECTION(SFX,SFY) c= union SFX /\ union SFY; theorem :: SETFAM_1:40 SFX <> {} & SFY <> {} implies meet SFX \/ meet SFY c= meet UNION(SFX,SFY); theorem :: SETFAM_1:41 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 means :: SETFAM_1:def 7 it c= bool D; end; definition let D be set; redefine mode Subset-Family of D -> Subset of bool D; end; definition let D be set; cluster empty Subset-Family of D; cluster non empty Subset-Family of 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; canceled 2; theorem :: SETFAM_1:44 (for P holds P in F iff P in G) implies F=G; scheme SubFamEx {A() -> set,P[Subset of A()]}: ex F being Subset-Family of A() st for B being Subset of A() holds B in F iff P[B]; definition let D,F; func COMPLEMENT(F) -> Subset-Family of D means :: SETFAM_1:def 8 for P being Subset of D holds P in it iff P` in F; involutiveness; end; canceled; theorem :: SETFAM_1:46 F <> {} implies COMPLEMENT(F) <> {}; theorem :: SETFAM_1:47 F <> {} implies [#] D \ union F = meet (COMPLEMENT(F)); theorem :: SETFAM_1:48 F <> {} implies union COMPLEMENT(F) = [#] D \ meet F;

Back to top