Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Families of Sets

by

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;
```