:: SETFAM_1 semantic presentation

definition

let c₁ be set ;
func meet c₁ -> set means :Def1: :: SETFAM_1:def 1
for b₁ being set holds
( b₁ in a₂ iff for b₂ being set st b₂ in a₁ holds
b₁ in b₂ ) if a₁ <> {}
otherwise a₂ = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines meet SETFAM_1:def 1 :

theorem Th1: :: SETFAM_1:1

canceled;

theorem Th2: :: SETFAM_1:2

meet {} = {} by Def1;

theorem Th3: :: SETFAM_1:3

for b₁ being set holds meet b₁ c= union b₁

proof end;

theorem Th4: :: SETFAM_1:4

for b₁, b₂ being set st b₁ in b₂ holds
meet b₂ c= b₁

proof end;

theorem Th5: :: SETFAM_1:5

for b₁ being set st {} in b₁ holds
meet b₁ = {}

proof end;

theorem Th6: :: SETFAM_1:6

for b₁, b₂ being set st b₁ <> {} & ( for b₃ being set st b₃ in b₁ holds
b₂ c= b₃ ) holds
b₂ c= meet b₁

proof end;

theorem Th7: :: SETFAM_1:7

for b₁, b₂ being set st b₁ <> {} & b₁ c= b₂ holds
meet b₂ c= meet b₁

proof end;

theorem Th8: :: SETFAM_1:8

for b₁, b₂, b₃ being set st b₁ in b₂ & b₁ c= b₃ holds
meet b₂ c= b₃

proof end;

theorem Th9: :: SETFAM_1:9

for b₁, b₂, b₃ being set st b₁ in b₂ & b₁ misses b₃ holds
meet b₂ misses b₃

proof end;

theorem Th10: :: SETFAM_1:10

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
meet (b₁ \/ b₂) = (meet b₁) /\ (meet b₂)

proof end;

theorem Th11: :: SETFAM_1:11

for b₁ being set holds meet {b₁} = b₁

proof end;

theorem Th12: :: SETFAM_1:12

for b₁, b₂ being set holds meet {b₁,b₂} = b₁ /\ b₂

proof end;

definition

let c₁, c₂ be set ;
pred c₁ is_finer_than c₂ means :: SETFAM_1:def 2
for b₁ being set st b₁ in a₁ holds
ex b₂ being set st
( b₂ in a₂ & b₁ c= b₂ );
reflexivity ;
pred c₂ is_coarser_than c₁ means :: SETFAM_1:def 3
for b₁ being set st b₁ in a₂ holds
ex b₂ being set st
( b₂ in a₁ & b₂ c= b₁ );
reflexivity ;

end;

:: deftheorem Def2 defines is_finer_than SETFAM_1:def 2 :

:: deftheorem Def3 defines is_coarser_than SETFAM_1:def 3 :

theorem Th13: :: SETFAM_1:13

canceled;

theorem Th14: :: SETFAM_1:14

canceled;

theorem Th15: :: SETFAM_1:15

canceled;

theorem Th16: :: SETFAM_1:16

canceled;

theorem Th17: :: SETFAM_1:17

for b₁, b₂ being set st b₁ c= b₂ holds
b₁ is_finer_than b₂

proof end;

theorem Th18: :: SETFAM_1:18

for b₁, b₂ being set st b₁ is_finer_than b₂ holds
union b₁ c= union b₂

proof end;

theorem Th19: :: SETFAM_1:19

for b₁, b₂ being set st b₁ <> {} & b₁ is_coarser_than b₂ holds
meet b₂ c= meet b₁

proof end;

theorem Th20: :: SETFAM_1:20

for b₁ being set holds {} is_finer_than b₁

proof end;

theorem Th21: :: SETFAM_1:21

for b₁ being set st b₁ is_finer_than {} holds
b₁ = {}

proof end;

theorem Th22: :: SETFAM_1:22

canceled;

theorem Th23: :: SETFAM_1:23

for b₁, b₂, b₃ being set st b₁ is_finer_than b₂ & b₂ is_finer_than b₃ holds
b₁ is_finer_than b₃

proof end;

theorem Th24: :: SETFAM_1:24

for b₁, b₂ being set st b₂ is_finer_than {b₁} holds
for b₃ being set st b₃ in b₂ holds
b₃ c= b₁

proof end;

theorem Th25: :: SETFAM_1:25

for b₁, b₂, b₃ being set st b₃ is_finer_than {b₁,b₂} holds
for b₄ being set holds
( not b₄ in b₃ or b₄ c= b₁ or b₄ c= b₂ )

proof end;

definition

let c₁, c₂ be set ;
func UNION c₁,c₂ -> set means :Def4: :: SETFAM_1:def 4
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being set st
( b₂ in a₁ & b₃ in a₂ & b₁ = b₂ \/ b₃ ) );
existence

proof end;

uniqueness

proof end;

commutativity

proof end;

func INTERSECTION c₁,c₂ -> set means :Def5: :: SETFAM_1:def 5
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being set st
( b₂ in a₁ & b₃ in a₂ & b₁ = b₂ /\ b₃ ) );
existence

proof end;

uniqueness

proof end;

commutativity

proof end;

func DIFFERENCE c₁,c₂ -> set means :Def6: :: SETFAM_1:def 6
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being set st
( b₂ in a₁ & b₃ in a₂ & b₁ = b₂ \ b₃ ) );
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 Th26: :: SETFAM_1:26

canceled;

theorem Th27: :: SETFAM_1:27

canceled;

theorem Th28: :: SETFAM_1:28

canceled;

theorem Th29: :: SETFAM_1:29

for b₁ being set holds b₁ is_finer_than UNION b₁,b₁

proof end;

theorem Th30: :: SETFAM_1:30

for b₁ being set holds INTERSECTION b₁,b₁ is_finer_than b₁

proof end;

theorem Th31: :: SETFAM_1:31

for b₁ being set holds DIFFERENCE b₁,b₁ is_finer_than b₁

proof end;

theorem Th32: :: SETFAM_1:32

canceled;

theorem Th33: :: SETFAM_1:33

canceled;

theorem Th34: :: SETFAM_1:34

for b₁, b₂ being set st b₁ meets b₂ holds
(meet b₁) /\ (meet b₂) = meet (INTERSECTION b₁,b₂)

proof end;

theorem Th35: :: SETFAM_1:35

for b₁, b₂ being set st b₂ <> {} holds
b₁ \/ (meet b₂) = meet (UNION {b₁},b₂)

proof end;

theorem Th36: :: SETFAM_1:36

for b₁, b₂ being set holds b₁ /\ (union b₂) = union (INTERSECTION {b₁},b₂)

proof end;

theorem Th37: :: SETFAM_1:37

for b₁, b₂ being set st b₂ <> {} holds
b₁ \ (union b₂) = meet (DIFFERENCE {b₁},b₂)

proof end;

theorem Th38: :: SETFAM_1:38

for b₁, b₂ being set st b₂ <> {} holds
b₁ \ (meet b₂) = union (DIFFERENCE {b₁},b₂)

proof end;

theorem Th39: :: SETFAM_1:39

for b₁, b₂ being set holds union (INTERSECTION b₁,b₂) = (union b₁) /\ (union b₂)

proof end;

theorem Th40: :: SETFAM_1:40

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
(meet b₁) \/ (meet b₂) c= meet (UNION b₁,b₂)

proof end;

theorem Th41: :: SETFAM_1:41

for b₁, b₂ being set holds meet (DIFFERENCE b₁,b₂) c= (meet b₁) \ (meet b₂)

proof end;

definition

let c₁ be set ;
mode Subset-Family of a₁ is Subset of (bool a₁);

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
redefine func union as union c₂ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
redefine func meet as meet c₂ -> Subset of a₁;
coherence

proof end;

end;

theorem Th42: :: SETFAM_1:42

canceled;

theorem Th43: :: SETFAM_1:43

canceled;

theorem Th44: :: SETFAM_1:44

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st ( for b₄ being Subset of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
canceled;
func COMPLEMENT c₂ -> Subset-Family of a₁ means :Def8: :: SETFAM_1:def 8
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff b₁ ` in a₂ );
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def7 SETFAM_1:def 7 :

:: deftheorem Def8 defines COMPLEMENT SETFAM_1:def 8 :

theorem Th45: :: SETFAM_1:45

canceled;

theorem Th46: :: SETFAM_1:46

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
COMPLEMENT b₂ <> {}

proof end;

theorem Th47: :: SETFAM_1:47

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

proof end;

theorem Th48: :: SETFAM_1:48

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

proof end;

theorem Th49: :: SETFAM_1:49

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ holds
( b₃ ` in COMPLEMENT b₂ iff b₃ in b₂ )

proof end;

theorem Th50: :: SETFAM_1:50

canceled;

theorem Th51: :: SETFAM_1:51

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st COMPLEMENT b₂ c= COMPLEMENT b₃ holds
b₂ c= b₃

proof end;

theorem Th52: :: SETFAM_1:52

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds
( COMPLEMENT b₂ c= b₃ iff b₂ c= COMPLEMENT b₃ )

proof end;

theorem Th53: :: SETFAM_1:53

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st COMPLEMENT b₂ = COMPLEMENT b₃ holds
b₂ = b₃

proof end;

theorem Th54: :: SETFAM_1:54

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds COMPLEMENT (b₂ \/ b₃) = (COMPLEMENT b₂) \/ (COMPLEMENT b₃)

proof end;

theorem Th55: :: SETFAM_1:55

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ = {b₁} holds
COMPLEMENT b₂ = {{} }

proof end;

registration

let c₁ be set ;
let c₂ be empty Subset-Family of c₁;
cluster COMPLEMENT a₂ -> empty ;
coherence

proof end;

end;

definition

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

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 c₁ be non empty set ;
cluster {a₁} -> with_non-empty_elements ;
coherence

proof end;

let c₂ be non empty set ;
cluster {a₁,a₂} -> with_non-empty_elements ;
coherence

proof end;

end;

registration

let c₁, c₂ be with_non-empty_elements set ;
cluster a₁ \/ a₂ -> with_non-empty_elements ;
coherence

proof end;

end;

theorem Th56: :: SETFAM_1:56

for b₁, b₂, b₃ being set st union b₁ c= b₂ & b₃ in b₁ holds
b₃ c= b₂

proof end;

theorem Th57: :: SETFAM_1:57

for b₁, b₂, b₃ being set st b₃ c= union (b₁ \/ b₂) & ( for b₄ being set st b₄ in b₂ holds
b₄ misses b₃ ) holds
b₃ c= union b₁

proof end;

definition

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

proof end;

consistency ;

end;

:: deftheorem Def10 defines Intersect SETFAM_1:def 10 :

theorem Th58: :: SETFAM_1:58

for b₁, b₂ being set
for b₃ being Subset-Family of b₁ st b₂ in b₁ holds
( b₂ in Intersect b₃ iff for b₄ being set st b₄ in b₃ holds
b₂ in b₄ )

proof end;

theorem Th59: :: SETFAM_1:59

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
Intersect b₃ c= Intersect b₂

proof end;

registration

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

end;

definition

let c₁ be set ;
attr a₁ is empty-membered means :Def11: :: SETFAM_1:def 11
for b₁ being non empty set holds not b₁ in a₁;

end;

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

notation

let c₁ be set ;
antonym with_non-empty_element c₁ for empty-membered c₁;

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 c₁ be with_non-empty_element set ;
cluster non empty Element of a₁;
existence

proof end;

end;