:: PARTIT1 semantic presentation

theorem Th1: :: PARTIT1:1

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ & b₃ c= b₄ holds
b₃ = b₄

proof end;

notation

let c₁, c₂ be set ;
synonym c₁ '<' c₂ for c₁ is_finer_than c₂;
synonym c₂ '>' c₁ for c₁ is_finer_than c₂;

end;

theorem Th2: :: PARTIT1:2

canceled;

theorem Th3: :: PARTIT1:3

for b₁ being set holds union (b₁ \ {{} }) = union b₁

proof end;

theorem Th4: :: PARTIT1:4

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st b₂ '>' b₃ & b₃ '>' b₂ holds
b₃ c= b₂

proof end;

theorem Th5: :: PARTIT1:5

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st b₂ '>' b₃ & b₃ '>' b₂ holds
b₂ = b₃

proof end;

theorem Th6: :: PARTIT1:6

canceled;

theorem Th7: :: PARTIT1:7

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st b₂ '>' b₃ holds
b₂ is_coarser_than b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be a_partition of c₁;
let c₃ be set ;
pred c₃ is_a_dependent_set_of c₂ means :Def1: :: PARTIT1:def 1
ex b₁ being set st
( b₁ c= a₂ & b₁ <> {} & a₃ = union b₁ );

end;

:: deftheorem Def1 defines is_a_dependent_set_of PARTIT1:def 1 :

definition

let c₁ be non empty set ;
let c₂, c₃ be a_partition of c₁;
let c₄ be set ;
pred c₄ is_min_depend c₂,c₃ means :Def2: :: PARTIT1:def 2
( a₄ is_a_dependent_set_of a₂ & a₄ is_a_dependent_set_of a₃ & ( for b₁ being set st b₁ c= a₄ & b₁ is_a_dependent_set_of a₂ & b₁ is_a_dependent_set_of a₃ holds
b₁ = a₄ ) );

end;

:: deftheorem Def2 defines is_min_depend PARTIT1:def 2 :

theorem Th8: :: PARTIT1:8

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st b₂ '>' b₃ holds
for b₄ being set st b₄ in b₂ holds
b₄ is_a_dependent_set_of b₃

proof end;

theorem Th9: :: PARTIT1:9

for b₁ being non empty set
for b₂ being a_partition of b₁ holds b₁ is_a_dependent_set_of b₂

proof end;

theorem Th10: :: PARTIT1:10

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being Subset-Family of b₁ st Intersect b₃ <> {} & ( for b₄ being set st b₄ in b₃ holds
b₄ is_a_dependent_set_of b₂ ) holds
Intersect b₃ is_a_dependent_set_of b₂

proof end;

theorem Th11: :: PARTIT1:11

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_a_dependent_set_of b₂ & b₄ is_a_dependent_set_of b₂ & b₃ meets b₄ holds
b₃ /\ b₄ is_a_dependent_set_of b₂

proof end;

theorem Th12: :: PARTIT1:12

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being Subset of b₁ st b₃ is_a_dependent_set_of b₂ & b₃ <> b₁ holds
b₃ ` is_a_dependent_set_of b₂

proof end;

theorem Th13: :: PARTIT1:13

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁
for b₄ being Element of b₁ ex b₅ being Subset of b₁ st
( b₄ in b₅ & b₅ is_min_depend b₂,b₃ )

proof end;

theorem Th14: :: PARTIT1:14

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being Element of b₁ ex b₄ being Subset of b₁ st
( b₃ in b₄ & b₄ in b₂ )

proof end;

definition

let c₁ be set ;
func PARTITIONS c₁ -> set means :Def3: :: PARTIT1:def 3
for b₁ being set holds
( b₁ in a₂ iff b₁ is a_partition of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :

registration

let c₁ be set ;
cluster PARTITIONS a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be a_partition of c₁;
func c₂ '/\' c₃ -> a_partition of a₁ equals :: PARTIT1:def 4
(INTERSECTION a₂,a₃) \ {{} };
correctness

proof end;

commutativity ;

end;

:: deftheorem Def4 defines '/\' PARTIT1:def 4 :

theorem Th15: :: PARTIT1:15

for b₁ being non empty set
for b₂ being a_partition of b₁ holds b₂ '/\' b₂ = b₂

proof end;

theorem Th16: :: PARTIT1:16

for b₁ being non empty set
for b₂, b₃, b₄ being a_partition of b₁ holds (b₂ '/\' b₃) '/\' b₄ = b₂ '/\' (b₃ '/\' b₄)

proof end;

theorem Th17: :: PARTIT1:17

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds b₂ '>' b₂ '/\' b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be a_partition of c₁;
func c₂ '\/' c₃ -> a_partition of a₁ means :Def5: :: PARTIT1:def 5
for b₁ being set holds
( b₁ in a₄ iff b₁ is_min_depend a₂,a₃ );
existence

proof end;

uniqueness

proof end;

commutativity

proof end;

end;

:: deftheorem Def5 defines '\/' PARTIT1:def 5 :

theorem Th18: :: PARTIT1:18

canceled;

theorem Th19: :: PARTIT1:19

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds b₂ '<' b₂ '\/' b₃

proof end;

theorem Th20: :: PARTIT1:20

for b₁ being non empty set
for b₂ being a_partition of b₁ holds b₂ '\/' b₂ = b₂

proof end;

theorem Th21: :: PARTIT1:21

for b₁ being non empty set
for b₂, b₃, b₄ being set
for b₅, b₆ being a_partition of b₁ st b₅ '<' b₆ & b₂ in b₆ & b₃ in b₅ & b₄ in b₂ & b₄ in b₃ holds
b₃ c= b₂

proof end;

theorem Th22: :: PARTIT1:22

for b₁ being non empty set
for b₂, b₃, b₄ being set
for b₅, b₆ being a_partition of b₁ st b₂ in b₅ '\/' b₆ & b₃ in b₅ & b₄ in b₂ & b₄ in b₃ holds
b₃ c= b₂

proof end;

theorem Th23: :: PARTIT1:23

for b₁ being non empty set
for b₂ being a_partition of b₁ ex b₃ being Equivalence_Relation of b₁ st
for b₄, b₅ being set holds
( [b₄,b₅] in b₃ iff ex b₆ being Subset of b₁ st
( b₆ in b₂ & b₄ in b₆ & b₅ in b₆ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be a_partition of c₁;
func ERl c₂ -> Equivalence_Relation of a₁ means :Def6: :: PARTIT1:def 6
for b₁, b₂ being set holds
( [b₁,b₂] in a₃ iff ex b₃ being Subset of a₁ st
( b₃ in a₂ & b₁ in b₃ & b₂ in b₃ ) );
existence by Th23;
uniqueness

proof end;

end;

:: deftheorem Def6 defines ERl PARTIT1:def 6 :

definition

let c₁ be non empty set ;
defpred S₁[ set , set ] means ex b₁ being a_partition of c₁ st
( b₁ = a₁ & a₂ = ERl b₁ );
E21: for b₁ being set st b₁ in PARTITIONS c₁ holds
ex b₂ being set st S₁[b₁,b₂]

proof end;

func Rel c₁ -> Function means :: PARTIT1:def 7
( dom a₂ = PARTITIONS a₁ & ( for b₁ being set st b₁ in PARTITIONS a₁ holds
ex b₂ being a_partition of a₁ st
( b₂ = b₁ & a₂ . b₁ = ERl b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Rel PARTIT1:def 7 :

theorem Th24: :: PARTIT1:24

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds
( b₂ '<' b₃ iff ERl b₂ c= ERl b₃ )

proof end;

theorem Th25: :: PARTIT1:25

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁
for b₄, b₅, b₆ being set
for b₇ being FinSequence of b₁ st b₄ c= b₁ & b₅ in b₄ & b₇ . 1 = b₅ & b₇ . (len b₇) = b₆ & 1 <= len b₇ & ( for b₈ being Nat st 1 <= b₈ & b₈ < len b₇ holds
ex b₉, b₁₀, b₁₁ being set st
( b₉ in b₂ & b₁₀ in b₃ & b₇ . b₈ in b₉ & b₁₁ in b₉ & b₁₁ in b₁₀ & b₇ . (b₈ + 1) in b₁₀ ) ) & b₄ is_a_dependent_set_of b₂ & b₄ is_a_dependent_set_of b₃ holds
b₆ in b₄

proof end;

theorem Th26: :: PARTIT1:26

for b₁ being non empty set
for b₂, b₃ being Equivalence_Relation of b₁
for b₄ being FinSequence of b₁
for b₅, b₆ being set st b₅ in b₁ & b₆ in b₁ & b₄ . 1 = b₅ & b₄ . (len b₄) = b₆ & 1 <= len b₄ & ( for b₇ being Nat st 1 <= b₇ & b₇ < len b₄ holds
ex b₈ being set st
( b₈ in b₁ & [(b₄ . b₇),b₈] in b₂ \/ b₃ & [b₈,(b₄ . (b₇ + 1))] in b₂ \/ b₃ ) ) holds
[b₅,b₆] in b₂ "\/" b₃

proof end;

theorem Th27: :: PARTIT1:27

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds ERl (b₂ '\/' b₃) = (ERl b₂) "\/" (ERl b₃)

proof end;

theorem Th28: :: PARTIT1:28

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds ERl (b₂ '/\' b₃) = (ERl b₂) /\ (ERl b₃)

proof end;

theorem Th29: :: PARTIT1:29

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st ERl b₂ = ERl b₃ holds
b₂ = b₃

proof end;

theorem Th30: :: PARTIT1:30

for b₁ being non empty set
for b₂, b₃, b₄ being a_partition of b₁ holds (b₂ '\/' b₃) '\/' b₄ = b₂ '\/' (b₃ '\/' b₄)

proof end;

theorem Th31: :: PARTIT1:31

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds b₂ '/\' (b₂ '\/' b₃) = b₂

proof end;

theorem Th32: :: PARTIT1:32

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ holds b₂ '\/' (b₂ '/\' b₃) = b₂

proof end;

theorem Th33: :: PARTIT1:33

for b₁ being non empty set
for b₂, b₃, b₄ being a_partition of b₁ st b₂ '<' b₄ & b₃ '<' b₄ holds
b₂ '\/' b₃ '<' b₄

proof end;

theorem Th34: :: PARTIT1:34

for b₁ being non empty set
for b₂, b₃, b₄ being a_partition of b₁ st b₂ '>' b₄ & b₃ '>' b₄ holds
b₂ '/\' b₃ '>' b₄

proof end;

notation

let c₁ be non empty set ;
synonym %I c₁ for SmallestPartition c₁;

end;

definition

let c₁ be non empty set ;
canceled;
func %O c₁ -> a_partition of a₁ equals :: PARTIT1:def 9
{a₁};
correctness

proof end;

end;

:: deftheorem Def8 PARTIT1:def 8 :

:: deftheorem Def9 defines %O PARTIT1:def 9 :

theorem Th35: :: PARTIT1:35

for b₁ being non empty set holds %I b₁ = { b₂ where B is Subset of b₁ : ex b₁ being set st
( b₂ = {b₃} & b₃ in b₁ ) }

proof end;

theorem Th36: :: PARTIT1:36

for b₁ being non empty set
for b₂ being a_partition of b₁ holds
( %O b₁ '>' b₂ & b₂ '>' %I b₁ )

proof end;

theorem Th37: :: PARTIT1:37

for b₁ being non empty set holds ERl (%O b₁) = nabla b₁

proof end;

theorem Th38: :: PARTIT1:38

for b₁ being non empty set holds ERl (%I b₁) = id b₁

proof end;

theorem Th39: :: PARTIT1:39

for b₁ being non empty set holds %I b₁ '<' %O b₁

proof end;

theorem Th40: :: PARTIT1:40

for b₁ being non empty set
for b₂ being a_partition of b₁ holds
( (%O b₁) '\/' b₂ = %O b₁ & (%O b₁) '/\' b₂ = b₂ )

proof end;

theorem Th41: :: PARTIT1:41

for b₁ being non empty set
for b₂ being a_partition of b₁ holds
( (%I b₁) '\/' b₂ = b₂ & (%I b₁) '/\' b₂ = %I b₁ )

proof end;