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

definition

let X be set ;

func meet X -> set means :Def1: :: SETFAM_1:def 1
for x being object 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 b₁ being set st
for x being object holds
( x in b₁ iff for Y being set st Y in X holds
x in Y ) ) & ( not X <> {} implies ex b₁ being set st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being set holds
( ( X <> {} & ( for x being object holds
( x in b₁ iff for Y being set st Y in X holds
x in Y ) ) & ( for x being object holds
( x in b₂ iff for Y being set st Y in X holds
x in Y ) ) implies b₁ = b₂ ) & ( not X <> {} & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being set holds verum ;

end;

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

:: 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 X, Z being set st Z in X holds
meet X c= Z by Def1;

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 ;

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 SFX, SFY 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 ;

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 b₁ being set st
for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in b₂ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, SFX, SFY being set st ( for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
for Z being set holds
( Z in b₁ 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 b₁ being set st
for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds
( Z in b₂ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, SFX, SFY being set st ( for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
for Z being set holds
( Z in b₁ 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 b₁ being set st
for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for Z being set holds
( Z in b₁ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds
( Z in b₂ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines UNION SETFAM_1:def 4 :
for SFX, SFY, b₃ being set holds
( b₃ = UNION (SFX,SFY) iff for Z being set holds
( Z in b₃ 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, b₃ being set holds
( b₃ = INTERSECTION (SFX,SFY) iff for Z being set holds
( Z in b₃ 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, b₃ being set holds
( b₃ = DIFFERENCE (SFX,SFY) iff for Z being set holds
( Z in b₃ 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 b₁ being Subset-Family of D st
for P being Subset of D holds
( P in b₁ iff P ` in F )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of D st ( for P being Subset of D holds
( P in b₁ iff P ` in F ) ) & ( for P being Subset of D holds
( P in b<sub>2</sub> iff P ` in F ) ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Subset-Family of D st ( for P being Subset of D holds
( P in b₁ iff P ` in b<sub>2</sub> ) ) holds
for P being Subset of D holds
( P in b<sub>2</sub> iff P ` in b₁ )

proof end;

end;

:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def 7 :
for D being set
for F, b₃ being Subset-Family of D holds
( b₃ = COMPLEMENT F iff for P being Subset of D holds
( P in b₃ 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;

:: 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 by Def7;

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 b₁ being set st
( not b₁ is empty & b₁ 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 by TARSKI:def 1;
let B be non empty set ;

cluster {A,B} -> with_non-empty_elements ;

coherence
{A,B} is with_non-empty_elements by TARSKI:def 2;
let C be non empty set ;

cluster {A,B,C} -> with_non-empty_elements ;

coherence
{A,B,C} is with_non-empty_elements by ENUMSET1:def 1;
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 by ENUMSET1:def 2;
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 by ENUMSET1:def 3;
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 by ENUMSET1:def 4;
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 by ENUMSET1:def 5;
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 by ENUMSET1:def 6;
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 by ENUMSET1:def 7;
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 by ENUMSET1:def 8;

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 X, Y, Z 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 b₁ 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 b₁ being Element of X holds not b₁ 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 b₁ being set st b₁ is with_non-empty_element

proof end;

end;

registration

cluster with_non-empty_element -> non empty for set ;

coherence
for b₁ being set st b₁ is with_non-empty_element holds
not b₁ is empty ;

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 b₁ being Element of X holds b₁ 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 b₁ being set st not b₁ is empty & b₁ is with_non-empty_elements holds
b₁ is with_non-empty_element ;

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 b₁ being set st X c= union b₁

proof end;

end;

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

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 ) by Def11;

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

registration

let TS be non empty set ;

cluster with_proper_subsets for Element of bool (bool TS);

existence
ex b₁ being Subset-Family of TS st b₁ 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 b₁ being set st not b₁ is trivial holds
b₁ 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 object st A <> {b} holds
ex a being Element of A st a <> b

proof end;