SETFAM_1: Families of Sets

:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990-2011 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

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines meet SETFAM_1:def 1 :

theorem :: SETFAM_1:1

canceled;

theorem :: SETFAM_1:2

meet {} = {} by Def1;

theorem Th3: :: SETFAM_1:3

for X being set holds meet X c= union X

proof end;

theorem Th4: :: SETFAM_1:4

for Z, X being set st Z in X holds
meet X c= Z

proof end;

theorem :: SETFAM_1:5

for X being set st {} in X holds
meet X = {} by Th4, XBOOLE_1:3;

theorem :: SETFAM_1:6

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 Th7: :: SETFAM_1:7

for X, Y being set st X <> {} & X c= Y holds
meet Y c= meet X

proof end;

theorem :: SETFAM_1:8

for X, Y, Z being set st X in Y & X c= Z holds
meet Y c= Z

proof end;

theorem :: SETFAM_1:9

for X, Y, Z being set st X in Y & X misses Z holds
meet Y misses Z by Th4, XBOOLE_1:63;

theorem :: SETFAM_1:10

for X, Y being set st X <> {} & Y <> {} holds
meet (X \/ Y) = (meet X) /\ (meet Y)

proof end;

theorem :: SETFAM_1:11

for x being set holds meet {x} = x

proof end;

theorem :: SETFAM_1:12

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

end;

:: deftheorem defines is_finer_than SETFAM_1:def 2 :

:: deftheorem defines is_coarser_than SETFAM_1:def 3 :

theorem :: SETFAM_1:13

canceled;

theorem :: SETFAM_1:14

canceled;

theorem :: SETFAM_1:15

canceled;

theorem :: SETFAM_1:16

canceled;

theorem :: SETFAM_1:17

for SFX, SFY being set st SFX c= SFY holds
SFX is_finer_than SFY

proof end;

theorem :: SETFAM_1:18

for SFX, SFY being set st SFX is_finer_than SFY holds
union SFX c= union SFY

proof end;

theorem :: SETFAM_1:19

for SFY, SFX being set st SFY <> {} & SFY is_coarser_than SFX holds
meet SFX c= meet SFY

proof end;

theorem :: SETFAM_1:20

for SFX being set holds {} is_finer_than SFX

proof end;

theorem :: SETFAM_1:21

for SFX being set st SFX is_finer_than {} holds
SFX = {}

proof end;

theorem :: SETFAM_1:22

canceled;

theorem :: SETFAM_1:23

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

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

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

proof end;

uniqueness

proof end;

commutativity

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

proof end;

uniqueness

proof end;

commutativity

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines UNION SETFAM_1:def 4 :

:: deftheorem Def5 defines INTERSECTION SETFAM_1:def 5 :

:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def 6 :

theorem :: SETFAM_1:26

canceled;

theorem :: SETFAM_1:27

canceled;

theorem :: SETFAM_1:28

canceled;

theorem :: SETFAM_1:29

for SFX being set holds SFX is_finer_than UNION (SFX,SFX)

proof end;

theorem :: SETFAM_1:30

for SFX being set holds INTERSECTION (SFX,SFX) is_finer_than SFX

proof end;

theorem :: SETFAM_1:31

for SFX being set holds DIFFERENCE (SFX,SFX) is_finer_than SFX

proof end;

theorem :: SETFAM_1:32

canceled;

theorem :: SETFAM_1:33

canceled;

theorem :: SETFAM_1:34

for SFX, SFY being set st SFX meets SFY holds
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))

proof end;

theorem :: SETFAM_1:35

for X, SFY being set st SFY <> {} holds
X \/ (meet SFY) = meet (UNION ({X},SFY))

proof end;

theorem :: SETFAM_1:36

for X, SFY being set holds X /\ (union SFY) = union (INTERSECTION ({X},SFY))

proof end;

theorem :: SETFAM_1:37

for X, SFY being set st SFY <> {} holds
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))

proof end;

theorem :: SETFAM_1:38

for X, SFY being set st SFY <> {} holds
X \ (meet SFY) = union (DIFFERENCE ({X},SFY))

proof end;

theorem :: SETFAM_1:39

for SFX, SFY being set holds union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)

proof end;

theorem :: SETFAM_1:40

for SFX, SFY being set st SFX <> {} & SFY <> {} holds
(meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))

proof end;

theorem :: SETFAM_1:41

for SFX, SFY being set holds meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)

proof end;

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

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

proof end;

end;

theorem :: SETFAM_1:42

canceled;

theorem :: SETFAM_1:43

canceled;

theorem Th44: :: SETFAM_1:44

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;
canceled;
func COMPLEMENT F -> Subset-Family of D means :Def8: :: SETFAM_1:def 8
for P being Subset of D holds
( P in it iff P ` in F );
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem SETFAM_1:def 7 :

:: deftheorem Def8 defines COMPLEMENT SETFAM_1:def 8 :

theorem :: SETFAM_1:45

canceled;

theorem Th46: :: SETFAM_1:46

for D being set
for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}

proof end;

theorem :: SETFAM_1:47

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

for D being set
for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)

proof end;

begin

theorem :: SETFAM_1:49

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 :: SETFAM_1:50

canceled;

theorem Th51: :: SETFAM_1:51

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

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

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

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

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

proof end;

end;

definition

let IT be set ;
attr IT is with_non-empty_elements means :Def9: :: SETFAM_1:def 9
not {} in IT;

end;

:: deftheorem Def9 defines with_non-empty_elements SETFAM_1:def 9 :

registration

cluster non empty with_non-empty_elements set ;
existence

proof end;

end;

registration

let A be non empty set ;
cluster {A} -> with_non-empty_elements ;
coherence

proof end;

let B be non empty set ;
cluster {A,B} -> with_non-empty_elements ;
coherence

proof end;

let C be non empty set ;
cluster {A,B,C} -> with_non-empty_elements ;
coherence

proof end;

let D be non empty set ;
cluster {A,B,C,D} -> with_non-empty_elements ;
coherence

proof end;

let E be non empty set ;
cluster {A,B,C,D,E} -> with_non-empty_elements ;
coherence

proof end;

let F be non empty set ;
cluster {A,B,C,D,E,F} -> with_non-empty_elements ;
coherence

proof end;

let G be non empty set ;
cluster {A,B,C,D,E,F,G} -> with_non-empty_elements ;
coherence

proof end;

let H be non empty set ;
cluster {A,B,C,D,E,F,G,H} -> with_non-empty_elements ;
coherence

proof end;

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

proof end;

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

proof end;

end;

registration

let A, B be with_non-empty_elements set ;
cluster A \/ B -> with_non-empty_elements ;
coherence

proof end;

end;

theorem :: SETFAM_1:56

for Y, Z, X being set st union Y c= Z & X in Y holds
X c= Z

proof end;

theorem :: SETFAM_1:57

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;

definition

let M be set ;
let B be Subset-Family of M;
func Intersect B -> Subset of M equals :Def10: :: SETFAM_1:def 10
meet B if B <> {}
otherwise M;
coherence

proof end;

consistency ;

end;

:: deftheorem Def10 defines Intersect SETFAM_1:def 10 :

theorem Th58: :: SETFAM_1:58

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

for X being set
for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H

proof end;

registration

let X be non empty with_non-empty_elements set ;
cluster -> non empty Element of X;
coherence by Def9;

end;

definition

let E be set ;
attr E is empty-membered means :Def11: :: SETFAM_1:def 11
for x being non empty set holds not x in E;

end;

:: deftheorem Def11 defines empty-membered SETFAM_1:def 11 :

notation

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

end;

registration

cluster with_non-empty_element set ;
existence

proof end;

end;

registration

cluster with_non-empty_element -> non empty set ;
coherence

proof end;

end;

registration

let X be with_non-empty_element set ;
cluster non empty Element of X;
existence

proof end;

end;

registration

let D be non empty with_non-empty_elements set ;
cluster union D -> non empty ;
coherence

proof end;

end;

registration

cluster non empty with_non-empty_elements -> with_non-empty_element set ;
coherence

proof end;

end;

definition

let X be set ;
mode Cover of X -> set means :Def12: :: SETFAM_1:def 12
X c= union it;
existence

proof end;

end;

:: deftheorem Def12 defines Cover SETFAM_1:def 12 :

theorem :: SETFAM_1:60

for X being set
for F being Subset-Family of X holds
( F is Cover of X iff union F = X )

proof end;

theorem Th61: :: SETFAM_1:61

for X being set holds {{}} is Subset-Family of X

proof end;

definition

let X be set ;
let F be Subset-Family of X;
attr F is with_proper_subsets means :Def13: :: SETFAM_1:def 13
not X in F;

end;

:: deftheorem Def13 defines with_proper_subsets SETFAM_1:def 13 :

theorem :: SETFAM_1:62

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 Element of bool (bool TS);
existence

proof end;

end;

theorem :: SETFAM_1:63

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;

registration

cluster non trivial -> with_non-empty_element set ;
coherence

proof end;

end;

definition

let X be set ;
:: original: bool
redefine func bool X -> Subset-Family of X;
coherence by ZFMISC_1:def 1;
canceled;

end;

:: deftheorem SETFAM_1:def 14 :