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;