:: by Beata Padlewska

::

:: Received April 5, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let X be set ;

( ( X <> {} implies ex b_{1} being set st

for x being set holds

( x in b_{1} iff for Y being set st Y in X holds

x in Y ) ) & ( not X <> {} implies ex b_{1} being set st b_{1} = {} ) )

for b_{1}, b_{2} being set holds

( ( X <> {} & ( for x being set holds

( x in b_{1} iff for Y being set st Y in X holds

x in Y ) ) & ( for x being set holds

( x in b_{2} iff for Y being set st Y in X holds

x in Y ) ) implies b_{1} = b_{2} ) & ( not X <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being set holds verum
;

end;
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 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 = {} ;

( ( X <> {} implies ex b

for x being set holds

( x in b

x in Y ) ) & ( not X <> {} implies ex b

proof end;

uniqueness for b

( ( X <> {} & ( for x being set holds

( x in b

x in Y ) ) & ( for x being set holds

( x in b

x in Y ) ) implies b

proof end;

consistency for b

:: deftheorem Def1 defines meet SETFAM_1:def 1 :

for X being set

for b_{2} being set holds

( ( X <> {} implies ( b_{2} = meet X iff for x being set holds

( x in b_{2} iff for Y being set st Y in X holds

x in Y ) ) ) & ( not X <> {} implies ( b_{2} = meet X iff b_{2} = {} ) ) );

for X being set

for b

( ( X <> {} implies ( b

( x in b

x in Y ) ) ) & ( not X <> {} implies ( b

:: Intersection of families of sets

theorem :: SETFAM_1:8

definition

let SFX, SFY be set ;

for SFX, X being set st X in SFX holds

ex Y being set st

( Y in SFX & X c= Y ) ;

for SFY, Y being set st Y in SFY holds

ex X being set st

( X in SFY & X c= Y ) ;

end;
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 X being set st X in SFX holds

ex Y being set st

( Y in SFY & X c= Y );

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 Y being set st Y in SFY holds

ex X being set st

( X in SFX & X c= Y );

for SFY, Y being set st Y in SFY holds

ex X being set st

( X in SFY & X c= Y ) ;

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

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

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

for SFX, SFY, SFZ being set st SFX is_finer_than SFY & SFY is_finer_than SFZ holds

SFX is_finer_than SFZ

SFX is_finer_than SFZ

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 )

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 ;

ex b_{1} being set st

for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \/ Y ) )

for b_{1}, b_{2} being set st ( for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds

( Z in b_{2} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds

b_{1} = b_{2}

for b_{1} being set

for SFX, SFY being set st ( for Z being set holds

( Z in b_{1} 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_{1} iff ex X, Y being set st

( X in SFY & Y in SFX & Z = X \/ Y ) )

ex b_{1} being set st

for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) )

for b_{1}, b_{2} being set st ( for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds

( Z in b_{2} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds

b_{1} = b_{2}

for b_{1} being set

for SFX, SFY being set st ( for Z being set holds

( Z in b_{1} 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_{1} iff ex X, Y being set st

( X in SFY & Y in SFX & Z = X /\ Y ) )

ex b_{1} being set st

for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) )

for b_{1}, b_{2} being set st ( for Z being set holds

( Z in b_{1} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds

( Z in b_{2} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds

b_{1} = b_{2}

end;
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 for Z being set holds

( Z in it iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \/ Y ) );

ex b

for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X \/ Y ) )

proof end;

uniqueness for b

( Z in b

( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds

b

proof end;

commutativity for b

for SFX, SFY being set st ( for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds

for Z being set holds

( Z in b

( 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 for Z being set holds

( Z in it iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) );

ex b

for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X /\ Y ) )

proof end;

uniqueness for b

( Z in b

( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds

b

proof end;

commutativity for b

for SFX, SFY being set st ( for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds

for Z being set holds

( Z in b

( 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 for Z being set holds

( Z in it iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) );

ex b

for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X \ Y ) )

proof end;

uniqueness for b

( Z in b

( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds

( Z in b

( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds

b

proof end;

:: deftheorem Def4 defines UNION SETFAM_1:def 4 :

for SFX, SFY being set

for b_{3} being set holds

( b_{3} = UNION (SFX,SFY) iff for Z being set holds

( Z in b_{3} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \/ Y ) ) );

for SFX, SFY being set

for b

( b

( Z in b

( X in SFX & Y in SFY & Z = X \/ Y ) ) );

:: deftheorem Def5 defines INTERSECTION SETFAM_1:def 5 :

for SFX, SFY being set

for b_{3} being set holds

( b_{3} = INTERSECTION (SFX,SFY) iff for Z being set holds

( Z in b_{3} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) ) );

for SFX, SFY being set

for b

( b

( Z in b

( X in SFX & Y in SFY & Z = X /\ Y ) ) );

:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def 6 :

for SFX, SFY being set

for b_{3} being set holds

( b_{3} = DIFFERENCE (SFX,SFY) iff for Z being set holds

( Z in b_{3} iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) ) );

for SFX, SFY being set

for b

( b

( Z in b

( X in SFX & Y in SFY & Z = X \ Y ) ) );

theorem :: SETFAM_1:23

for SFX, SFY being set st SFX meets SFY holds

(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))

(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,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))

(meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))

proof end;

:: Family of subsets of a set

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

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

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

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

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

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;

ex b_{1} being Subset-Family of D st

for P being Subset of D holds

( P in b_{1} iff P ` in F )

for b_{1}, b_{2} being Subset-Family of D st ( for P being Subset of D holds

( P in b_{1} iff P ` in F ) ) & ( for P being Subset of D holds

( P in b_{2} iff P ` in F ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Subset-Family of D st ( for P being Subset of D holds

( P in b_{1} iff P ` in b_{2} ) ) holds

for P being Subset of D holds

( P in b_{2} iff P ` in b_{1} )

end;
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 for P being Subset of D holds

( P in it iff P ` in F );

ex b

for P being Subset of D holds

( P in b

proof end;

uniqueness for b

( P in b

( P in b

b

proof end;

involutiveness for b

( P in b

for P being Subset of D holds

( P in b

proof end;

:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def 7 :

for D being set

for F, b_{3} being Subset-Family of D holds

( b_{3} = COMPLEMENT F iff for P being Subset of D holds

( P in b_{3} iff P ` in F ) );

for D being set

for F, b

( b

( P in b

theorem :: SETFAM_1:33

for D being set

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

([#] D) \ (union F) = meet (COMPLEMENT F)

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)

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 )

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

for X being set

for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)

for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)

proof end;

registration
end;

:: from AMI_1

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

for IT being set holds

( IT is with_non-empty_elements iff not {} in IT );

registration

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is with_non-empty_elements )

end;
ex b

( not b

proof end;

registration

let A be non empty set ;

coherence

{A} is with_non-empty_elements

coherence

{A,B} is with_non-empty_elements

coherence

{A,B,C} is with_non-empty_elements

coherence

{A,B,C,D} is with_non-empty_elements

coherence

{A,B,C,D,E} is with_non-empty_elements

coherence

{A,B,C,D,E,F} is with_non-empty_elements

coherence

{A,B,C,D,E,F,G} is with_non-empty_elements

coherence

{A,B,C,D,E,F,G,H} is with_non-empty_elements

coherence

{A,B,C,D,E,F,G,H,I} is with_non-empty_elements

coherence

{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements

end;
coherence

{A} is with_non-empty_elements

proof end;

let B be non empty set ;coherence

{A,B} is with_non-empty_elements

proof end;

let C be non empty set ;coherence

{A,B,C} is with_non-empty_elements

proof end;

let D be non empty set ;coherence

{A,B,C,D} is with_non-empty_elements

proof end;

let E be non empty set ;coherence

{A,B,C,D,E} is with_non-empty_elements

proof end;

let F be non empty set ;coherence

{A,B,C,D,E,F} is with_non-empty_elements

proof end;

let G be non empty set ;coherence

{A,B,C,D,E,F,G} is with_non-empty_elements

proof end;

let H be non empty set ;coherence

{A,B,C,D,E,F,G,H} is with_non-empty_elements

proof end;

let I be non empty set ;coherence

{A,B,C,D,E,F,G,H,I} is with_non-empty_elements

proof end;

let J be non empty set ;coherence

{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements

proof end;

registration
end;

:: from LATTICE4

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

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;

coherence

( ( B <> {} implies meet B is Subset of M ) & ( not B <> {} implies M is Subset of M ) )

for b_{1} being Subset of M holds verum
;

end;
let B be Subset-Family of M;

coherence

( ( B <> {} implies meet B is Subset of M ) & ( not B <> {} implies M is Subset of M ) )

proof end;

consistency for b

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

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 )

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;

:: from PUA2MSS1, 2005.08.22, A.T

registration

let X be non empty with_non-empty_elements set ;

coherence

for b_{1} being Element of X holds not b_{1} is empty
by Def8;

end;
coherence

for b

definition

let E be set ;

end;
attr E is empty-membered means :Def10: :: SETFAM_1:def 10

for x being non empty set holds not x in E;

for x being non empty set holds not x in E;

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

for E being set holds

( E is empty-membered iff for x being non empty set holds not x in E );

registration

coherence

for b_{1} being set st b_{1} is with_non-empty_element holds

not b_{1} is empty

end;
for b

not b

proof end;

:: from TRIANG_1, 2005.08.22

registration

let X be with_non-empty_element set ;

existence

not for b_{1} being Element of X holds b_{1} is empty

end;
existence

not for b

proof end;

:: from MSAFREE1, 2007.03.09, A.T.

registration
end;

:: missing, 2007.03.09, A.T.

registration

coherence

for b_{1} being set st not b_{1} is empty & b_{1} is with_non-empty_elements holds

b_{1} is with_non-empty_element

end;
for b

b

proof end;

:: the concept of a cover, 2008.03.08, A.T.

:: deftheorem Def11 defines Cover SETFAM_1:def 11 :

for X being set

for b_{2} being set holds

( b_{2} is Cover of X iff X c= union b_{2} );

for X being set

for b

( b

:: from MEASURE1, 2008.06.08, A.T.

:: from BORSUK_5 (generalized), 2008.06.08, A.T.

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

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

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 ;

existence

ex b_{1} being Subset-Family of TS st b_{1} is with_proper_subsets

end;
existence

ex b

proof 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

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

coherence

for b_{1} being set st not b_{1} is trivial holds

b_{1} is with_non-empty_element

end;
for b

b

proof 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;
:: original: bool

redefine func bool X -> Subset-Family of X;

coherence

bool X is Subset-Family of X by ZFMISC_1:def 1;

:: from HAHNBAN, 2011.04.26., A.T.