:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: 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 = {} ) ) );
theorem :: SETFAM_1:1
canceled;
theorem :: SETFAM_1:2
theorem Th3: :: SETFAM_1:3
theorem Th4: :: SETFAM_1:4
theorem :: SETFAM_1:5
theorem :: SETFAM_1:6
theorem Th7: :: SETFAM_1:7
theorem :: SETFAM_1:8
theorem :: SETFAM_1:9
theorem :: SETFAM_1:10
theorem :: SETFAM_1:11
theorem :: SETFAM_1:12
:: 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
theorem :: SETFAM_1:18
theorem :: SETFAM_1:19
theorem :: SETFAM_1:20
theorem :: SETFAM_1:21
theorem :: SETFAM_1:22
canceled;
theorem :: SETFAM_1:23
theorem :: SETFAM_1:24
theorem :: SETFAM_1:25
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 ) )
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
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 ) )
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 ) )
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
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 ) )
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 ) )
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
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:26
canceled;
theorem :: SETFAM_1:27
canceled;
theorem :: SETFAM_1:28
canceled;
theorem :: SETFAM_1:29
theorem :: SETFAM_1:30
theorem :: SETFAM_1:31
theorem :: SETFAM_1:32
canceled;
theorem :: SETFAM_1:33
canceled;
theorem :: SETFAM_1:34
theorem :: SETFAM_1:35
theorem :: SETFAM_1:36
theorem :: SETFAM_1:37
theorem :: SETFAM_1:38
theorem :: SETFAM_1:39
theorem :: SETFAM_1:40
theorem :: SETFAM_1:41
theorem :: SETFAM_1:42
canceled;
theorem :: SETFAM_1:43
canceled;
theorem Th44: :: SETFAM_1:44
:: deftheorem SETFAM_1:def 7 :
canceled;
:: deftheorem Def8 defines COMPLEMENT SETFAM_1:def 8 :
theorem :: SETFAM_1:45
canceled;
theorem Th46: :: SETFAM_1:46
theorem :: SETFAM_1:47
theorem :: SETFAM_1:48
theorem :: SETFAM_1:49
theorem :: SETFAM_1:50
canceled;
theorem Th51: :: SETFAM_1:51
theorem :: SETFAM_1:52
theorem :: SETFAM_1:53
theorem :: SETFAM_1:54
theorem :: SETFAM_1:55
:: deftheorem Def9 defines with_non-empty_elements SETFAM_1:def 9 :
registration
let A be non
empty set ;
cluster {A} -> with_non-empty_elements ;
coherence
{A} is with_non-empty_elements
let B be non
empty set ;
cluster {A,B} -> with_non-empty_elements ;
coherence
{A,B} is with_non-empty_elements
let C be non
empty set ;
cluster {A,B,C} -> with_non-empty_elements ;
coherence
{A,B,C} is with_non-empty_elements
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
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
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
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
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
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
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
end;
theorem :: SETFAM_1:56
theorem :: SETFAM_1:57
:: deftheorem Def10 defines Intersect SETFAM_1:def 10 :
theorem Th58: :: SETFAM_1:58
theorem :: SETFAM_1:59
:: deftheorem Def11 defines empty-membered SETFAM_1:def 11 :
:: deftheorem Dfx defines Cover SETFAM_1:def 12 :
theorem :: SETFAM_1:60
theorem Th61: :: SETFAM_1:61
:: deftheorem Def6 defines with_proper_subsets SETFAM_1:def 13 :
theorem :: SETFAM_1:62
theorem :: SETFAM_1:63