:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let X be set ;
func meet X -> set means :Def1: :: SETFAM_1:def 1
 for x being set holds
( x in it iff for Y being set st Y in X holds
x in Y ) if X <> {}
otherwise it = {} ;
existence
( ( X <> {} implies ex b1 being set st
for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) & ( not X <> {} implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( X <> {} & ( for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) implies b1 = b2 ) & ( not X <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum ;
end;

:: deftheorem Def1 defines meet SETFAM_1:def 1 :
for X being set
for b2 being set holds
( ( X <> {} implies ( b2 = meet X iff for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) ) & ( not X <> {} implies ( b2 = meet X iff b2 = {} ) ) );

:: Intersection of families of sets
theorem :: SETFAM_1:1
meet {} = {} by Def1;

theorem Th2: :: SETFAM_1:2
for X being set holds meet X c= union X
proof end;

theorem Th3: :: SETFAM_1:3
for Z, X being set st Z in X holds
meet X c= Z
proof end;

theorem :: SETFAM_1:4
for X being set st {} in X holds
meet X = {} by Th3, XBOOLE_1:3;

theorem :: SETFAM_1:5
for X, Z being set st X <> {} & ( for Z1 being set st Z1 in X holds
Z c= Z1 ) holds
Z c= meet X
proof end;

theorem Th6: :: SETFAM_1:6
for X, Y being set st X <> {} & X c= Y holds
meet Y c= meet X
proof end;

theorem :: SETFAM_1:7
for X, Y, Z being set st X in Y & X c= Z holds
meet Y c= Z
proof end;

theorem :: SETFAM_1:8
for X, Y, Z being set st X in Y & X misses Z holds
meet Y misses Z by Th3, XBOOLE_1:63;

theorem :: SETFAM_1:9
for X, Y being set st X <> {} & Y <> {} holds
meet (X \/ Y) = (meet X) /\ (meet Y)
proof end;

theorem :: SETFAM_1:10
for x being set holds meet {x} = x
proof end;

theorem :: SETFAM_1:11
for X, Y being set holds meet {X,Y} = X /\ Y
proof end;

definition
let SFX, SFY be set ;
pred SFX is_finer_than SFY means :: SETFAM_1:def 2
 for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y );
reflexivity
for SFX, X being set st X in SFX holds
ex Y being set st
( Y in SFX & X c= Y ) ;
pred SFY is_coarser_than SFX means :: SETFAM_1:def 3
 for Y being set st Y in SFY holds
ex X being set st
( X in SFX & X c= Y );
reflexivity
for SFY, Y being set st Y in SFY holds
ex X being set st
( X in SFY & X c= Y ) ;
end;

:: deftheorem defines is_finer_than SETFAM_1:def 2 :
for SFX, SFY being set holds
( SFX is_finer_than SFY iff for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y ) );

:: deftheorem defines is_coarser_than SETFAM_1:def 3 :
for SFX, SFY being set holds
( SFY is_coarser_than SFX iff for Y being set st Y in SFY holds
ex X being set st
( X in SFX & X c= Y ) );

theorem :: SETFAM_1:12
for SFX, SFY being set st SFX c= SFY holds
SFX is_finer_than SFY
proof end;

theorem :: SETFAM_1:13
for SFX, SFY being set st SFX is_finer_than SFY holds
union SFX c= union SFY
proof end;

theorem :: SETFAM_1:14
for SFY, SFX being set st SFY <> {} & SFY is_coarser_than SFX holds
meet SFX c= meet SFY
proof end;

theorem :: SETFAM_1:15
for SFX being set holds {} is_finer_than SFX
proof end;

theorem :: SETFAM_1:16
for SFX being set st SFX is_finer_than {} holds
SFX = {}
proof end;

theorem :: SETFAM_1:17
for SFX, SFY, SFZ being set st SFX is_finer_than SFY & SFY is_finer_than SFZ holds
SFX is_finer_than SFZ
proof end;

theorem :: SETFAM_1:18
for Y, SFX being set st SFX is_finer_than {Y} holds
for X being set st X in SFX holds
X c= Y
proof end;

theorem :: SETFAM_1:19
for X, Y, SFX being set st SFX is_finer_than {X,Y} holds
for Z being set holds
( not Z in SFX or Z c= X or Z c= Y )
proof end;

definition
let SFX, SFY be set ;
func UNION (SFX,SFY) -> set means :Def4: :: SETFAM_1:def 4
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
b1 = b2
proof end;
commutativity
for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) )
proof end;
func INTERSECTION (SFX,SFY) -> set means :Def5: :: SETFAM_1:def 5
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
b1 = b2
proof end;
commutativity
for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
proof end;
func DIFFERENCE (SFX,SFY) -> set means :Def6: :: SETFAM_1:def 6
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines UNION SETFAM_1:def 4 :
for SFX, SFY being set
for b3 being set holds
( b3 = UNION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) );

:: deftheorem Def5 defines INTERSECTION SETFAM_1:def 5 :
for SFX, SFY being set
for b3 being set holds
( b3 = INTERSECTION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) );

:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def 6 :
for SFX, SFY being set
for b3 being set holds
( b3 = DIFFERENCE (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) );

theorem :: SETFAM_1:20
for SFX being set holds SFX is_finer_than UNION (SFX,SFX)
proof end;

theorem :: SETFAM_1:21
for SFX being set holds INTERSECTION (SFX,SFX) is_finer_than SFX
proof end;

theorem :: SETFAM_1:22
for SFX being set holds DIFFERENCE (SFX,SFX) is_finer_than SFX
proof end;

theorem :: SETFAM_1:23
for SFX, SFY being set st SFX meets SFY holds
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
proof end;

theorem :: SETFAM_1:24
for X, SFY being set st SFY <> {} holds
X \/ (meet SFY) = meet (UNION ({X},SFY))
proof end;

theorem :: SETFAM_1:25
for X, SFY being set holds X /\ (union SFY) = union (INTERSECTION ({X},SFY))
proof end;

theorem :: SETFAM_1:26
for X, SFY being set st SFY <> {} holds
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
proof end;

theorem :: SETFAM_1:27
for X, SFY being set st SFY <> {} holds
X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
proof end;

theorem :: SETFAM_1:28
for SFX, SFY being set holds union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
proof end;

theorem :: SETFAM_1:29
for SFX, SFY being set st SFX <> {} & SFY <> {} holds
(meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))
proof end;

theorem :: SETFAM_1:30
for SFX, SFY being set holds meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
proof end;

:: Family of subsets of a set
definition
let D be set ;
mode Subset-Family of D is Subset of (bool D);
end;

definition
let D be set ;
let F be Subset-Family of D;
:: original: union
redefine func union F -> Subset of D;
coherence
union F is Subset of D
proof end;
end;

definition
let D be set ;
let F be Subset-Family of D;
:: original: meet
redefine func meet F -> Subset of D;
coherence
meet F is Subset of D
proof end;
end;

theorem Th31: :: SETFAM_1:31
for D being set
for F, G being Subset-Family of D st ( for P being Subset of D holds
( P in F iff P in G ) ) holds
F = G
proof end;

definition
let D be set ;
let F be Subset-Family of D;
func COMPLEMENT F -> Subset-Family of D means :Def7: :: SETFAM_1:def 7
 for P being Subset of D holds
( P in it iff P ` in F );
existence
ex b1 being Subset-Family of D st
for P being Subset of D holds
( P in b1 iff P ` in F )
proof end;
uniqueness
for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in F ) ) & ( for P being Subset of D holds
( P in b2 iff P ` in F ) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in b2 ) ) holds
for P being Subset of D holds
( P in b2 iff P ` in b1 )
proof end;
end;

:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def 7 :
for D being set
for F, b3 being Subset-Family of D holds
( b3 = COMPLEMENT F iff for P being Subset of D holds
( P in b3 iff P ` in F ) );

theorem Th32: :: SETFAM_1:32
for D being set
for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}
proof end;

theorem :: SETFAM_1:33
for D being set
for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)
proof end;

theorem :: SETFAM_1:34
for D being set
for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)
proof end;

begin

:: from YELLOW_8, 2004.07.25
theorem :: SETFAM_1:35
for X being set
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
proof end;

theorem Th36: :: SETFAM_1:36
for X being set
for F, G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds
F c= G
proof end;

theorem :: SETFAM_1:37
for X being set
for F, G being Subset-Family of X holds
( COMPLEMENT F c= G iff F c= COMPLEMENT G )
proof end;

theorem :: SETFAM_1:38
for X being set
for F, G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds
F = G
proof end;

theorem :: SETFAM_1:39
for X being set
for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
proof end;

theorem :: SETFAM_1:40
for X being set
for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}
proof end;

registration
let X be set ;
let F be empty Subset-Family of X;
cluster COMPLEMENT F -> empty ;
coherence
COMPLEMENT F is empty
proof end;
end;

:: from AMI_1
definition
let IT be set ;
attr IT is with_non-empty_elements means :Def8: :: SETFAM_1:def 8
 not {} in IT;
end;

:: deftheorem Def8 defines with_non-empty_elements SETFAM_1:def 8 :
for IT being set holds
( IT is with_non-empty_elements iff not {} in IT );

registration
cluster non empty with_non-empty_elements for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is with_non-empty_elements )
proof end;
end;

registration
let A be non empty set ;
cluster {A} -> with_non-empty_elements ;
coherence
{A} is with_non-empty_elements
proof end;
let B be non empty set ;
cluster {A,B} -> with_non-empty_elements ;
coherence
{A,B} is with_non-empty_elements
proof end;
let C be non empty set ;
cluster {A,B,C} -> with_non-empty_elements ;
coherence
{A,B,C} is with_non-empty_elements
proof end;
let D be non empty set ;
cluster {A,B,C,D} -> with_non-empty_elements ;
coherence
{A,B,C,D} is with_non-empty_elements
proof end;
let E be non empty set ;
cluster {A,B,C,D,E} -> with_non-empty_elements ;
coherence
{A,B,C,D,E} is with_non-empty_elements
proof end;
let F be non empty set ;
cluster {A,B,C,D,E,F} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F} is with_non-empty_elements
proof end;
let G be non empty set ;
cluster {A,B,C,D,E,F,G} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G} is with_non-empty_elements
proof end;
let H be non empty set ;
cluster {A,B,C,D,E,F,G,H} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H} is with_non-empty_elements
proof end;
let I be non empty set ;
cluster {A,B,C,D,E,F,G,H,I} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I} is with_non-empty_elements
proof end;
let J be non empty set ;
cluster {A,B,C,D,E,F,G,H,I,J} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
proof end;
end;

registration
let A, B be with_non-empty_elements set ;
cluster A \/ B -> with_non-empty_elements ;
coherence
A \/ B is with_non-empty_elements
proof end;
end;

:: from LATTICE4
theorem :: SETFAM_1:41
for Y, Z, X being set st union Y c= Z & X in Y holds
X c= Z
proof end;

:: from LOPCLSET
theorem :: SETFAM_1:42
for A, B, X being set st X c= union (A \/ B) & ( for Y being set st Y in B holds
Y misses X ) holds
X c= union A
proof end;

:: from CANTOR_1
definition
let M be set ;
let B be Subset-Family of M;
func Intersect B -> Subset of M equals :Def9: :: SETFAM_1:def 9
 meet B if B <> {}
otherwise M;
coherence
( ( B <> {} implies meet B is Subset of M ) & ( not B <> {} implies M is Subset of M ) )
proof end;
consistency
for b1 being Subset of M holds verum ;
end;

:: deftheorem Def9 defines Intersect SETFAM_1:def 9 :
for M being set
for B being Subset-Family of M holds
( ( B <> {} implies Intersect B = meet B ) & ( not B <> {} implies Intersect B = M ) );

theorem Th43: :: SETFAM_1:43
for X, x being set
for 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 )
proof end;

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
proof end;

:: 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;
coherence
for b1 being Element of X holds not b1 is empty by Def8;
end;

definition
let E be set ;
attr E is empty-membered means :Def10: :: SETFAM_1:def 10
 for x being non empty set holds not x in E;
end;

:: deftheorem Def10 defines empty-membered SETFAM_1:def 10 :
for E being set holds
( E is empty-membered iff for x being non empty set holds not x in E );

notation
let E be set ;
antonym with_non-empty_element E for empty-membered ;
end;

registration
cluster with_non-empty_element for set ;
existence
ex b1 being set st b1 is with_non-empty_element
proof end;
end;

registration
cluster with_non-empty_element -> non empty for set ;
coherence
for b1 being set st b1 is with_non-empty_element holds
not b1 is empty
proof end;
end;

:: from TRIANG_1, 2005.08.22
registration
let X be with_non-empty_element set ;
cluster non empty for Element of X;
existence
not for b1 being Element of X holds b1 is empty
proof end;
end;

:: from MSAFREE1, 2007.03.09, A.T.
registration
let D be non empty with_non-empty_elements set ;
cluster union D -> non empty ;
coherence
not union D is empty
proof end;
end;

:: missing, 2007.03.09, A.T.
registration
cluster non empty with_non-empty_elements -> with_non-empty_element for set ;
coherence
for b1 being set st not b1 is empty & b1 is with_non-empty_elements holds
b1 is with_non-empty_element
proof end;
end;

:: the concept of a cover, 2008.03.08, A.T.
definition
let X be set ;
mode Cover of X -> set means :Def11: :: SETFAM_1:def 11
X c= union it;
existence
ex b1 being set st X c= union b1
proof end;
end;

:: deftheorem Def11 defines Cover SETFAM_1:def 11 :
for X being set
for b2 being set holds
( b2 is Cover of X iff X c= union b2 );

theorem :: SETFAM_1:45
for X being set
for F being Subset-Family of X holds
( F is Cover of X iff union F = X )
proof end;

:: from MEASURE1, 2008.06.08, A.T.
theorem Th46: :: SETFAM_1:46
for X being set holds {{}} is Subset-Family of X
proof end;

:: 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 :Def12: :: SETFAM_1:def 12
 not X in F;
end;

:: deftheorem Def12 defines with_proper_subsets SETFAM_1:def 12 :
for X being set
for F being Subset-Family of X holds
( F is with_proper_subsets iff not X in F );

theorem :: SETFAM_1:47
for TS being set
for F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds
G is with_proper_subsets
proof end;

registration
let TS be non empty set ;
cluster with_proper_subsets for Element of bool (bool TS);
existence
ex b1 being Subset-Family of TS st b1 is with_proper_subsets
proof end;
end;

theorem :: SETFAM_1:48
for TS being non empty set
for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets
proof end;

:: from YELLOW21, 2008.09.10, A.T.
registration
cluster non trivial -> with_non-empty_element for set ;
coherence
for b1 being set st not b1 is trivial holds
b1 is with_non-empty_element
proof end;
end;

:: from PCOMPS_1, 2010.02.26, A.T.
definition
let X be set ;
:: original: bool
redefine func bool X -> Subset-Family of X;
coherence
bool X is Subset-Family of X by ZFMISC_1:def 1;
end;

:: from HAHNBAN, 2011.04.26., A.T.
theorem :: SETFAM_1:49
for A being non empty set
for b being set st A <> {b} holds
ex a being Element of A st a <> b
proof end;