:: EQREL_1 semantic presentation

definition

let c₁ be set ;
func nabla c₁ -> Relation of a₁ equals :: EQREL_1:def 1
[:a₁,a₁:];
coherence by RELSET_1:def 1;

end;

:: deftheorem Def1 defines nabla EQREL_1:def 1 :

registration

let c₁ be set ;
cluster nabla a₁ -> reflexive total ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be Relation of c₁;
redefine func /\ as c₂ /\ c₃ -> Relation of a₁;
coherence

proof end;

redefine func \/ as c₂ \/ c₃ -> Relation of a₁;
coherence

proof end;

end;

Lemma1: for b₁, b₂ being Nat st b₁ < b₂ holds
b₂ - b₁ is Nat
by NAT_1:61;

theorem Th1: :: EQREL_1:1

canceled;

theorem Th2: :: EQREL_1:2

canceled;

theorem Th3: :: EQREL_1:3

canceled;

theorem Th4: :: EQREL_1:4

for b₁ being set holds
( id b₁ is_reflexive_in b₁ & id b₁ is_symmetric_in b₁ & id b₁ is_transitive_in b₁ )

proof end;

definition

let c₁ be set ;
mode Tolerance of a₁ is reflexive symmetric total Relation of a₁;
mode Equivalence_Relation of a₁ is symmetric transitive total Relation of a₁;

end;

theorem Th5: :: EQREL_1:5

canceled;

theorem Th6: :: EQREL_1:6

for b₁ being set holds id b₁ is Equivalence_Relation of b₁ ;

theorem Th7: :: EQREL_1:7

for b₁ being set holds nabla b₁ is Equivalence_Relation of b₁

proof end;

registration

let c₁ be set ;
cluster nabla a₁ -> reflexive symmetric transitive total ;
coherence by Th7;

end;

Lemma3: for b₁, b₂, b₃ being set
for b₄ being Relation of b₃ st [b₁,b₂] in b₄ holds
( b₁ in b₃ & b₂ in b₃ )

proof end;

theorem Th8: :: EQREL_1:8

canceled;

theorem Th9: :: EQREL_1:9

canceled;

theorem Th10: :: EQREL_1:10

canceled;

theorem Th11: :: EQREL_1:11

for b₁, b₂ being set
for b₃ being reflexive total Relation of b₁ st b₂ in b₁ holds
[b₂,b₂] in b₃

proof end;

theorem Th12: :: EQREL_1:12

for b₁, b₂, b₃ being set
for b₄ being symmetric total Relation of b₁ st [b₂,b₃] in b₄ holds
[b₃,b₂] in b₄

proof end;

theorem Th13: :: EQREL_1:13

for b₁, b₂, b₃, b₄ being set
for b₅ being transitive total Relation of b₁ st [b₂,b₃] in b₅ & [b₃,b₄] in b₅ holds
[b₂,b₄] in b₅

proof end;

theorem Th14: :: EQREL_1:14

for b₁ being set
for b₂ being reflexive total Relation of b₁ st ex b₃ being set st b₃ in b₁ holds
b₂ <> {} by Th11;

theorem Th15: :: EQREL_1:15

canceled;

theorem Th16: :: EQREL_1:16

for b₁ being set
for b₂ being Relation of b₁ holds
( b₂ is Equivalence_Relation of b₁ iff ( b₂ is reflexive & b₂ is symmetric & b₂ is transitive & field b₂ = b₁ ) )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Equivalence_Relation of c₁;
redefine func /\ as c₂ /\ c₃ -> Equivalence_Relation of a₁;
coherence

proof end;

end;

theorem Th17: :: EQREL_1:17

for b₁ being set
for b₂ being Equivalence_Relation of b₁ holds (id b₁) /\ b₂ = id b₁

proof end;

theorem Th18: :: EQREL_1:18

for b₁ being set
for b₂ being Relation of b₁ holds (nabla b₁) /\ b₂ = b₂ by XBOOLE_1:28;

theorem Th19: :: EQREL_1:19

for b₁ being set
for b₂ being Subset-Family of [:b₁,b₁:] st b₂ <> {} & ( for b₃ being set st b₃ in b₂ holds
b₃ is Equivalence_Relation of b₁ ) holds
meet b₂ is Equivalence_Relation of b₁

proof end;

theorem Th20: :: EQREL_1:20

for b₁ being set
for b₂ being Relation of b₁ ex b₃ being Equivalence_Relation of b₁ st
( b₂ c= b₃ & ( for b₄ being Equivalence_Relation of b₁ st b₂ c= b₄ holds
b₃ c= b₄ ) )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Equivalence_Relation of c₁;
canceled;
func c₂ "\/" c₃ -> Equivalence_Relation of a₁ means :Def3: :: EQREL_1:def 3
( a₂ \/ a₃ c= a₄ & ( for b₁ being Equivalence_Relation of a₁ st a₂ \/ a₃ c= b₁ holds
a₄ c= b₁ ) );
existence by Th20;
uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem Def2 EQREL_1:def 2 :

:: deftheorem Def3 defines "\/" EQREL_1:def 3 :

theorem Th21: :: EQREL_1:21

canceled;

theorem Th22: :: EQREL_1:22

for b₁ being set
for b₂ being Equivalence_Relation of b₁ holds b₂ "\/" b₂ = b₂ ;

theorem Th23: :: EQREL_1:23

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ holds b₂ "\/" b₃ = b₃ "\/" b₂ ;

theorem Th24: :: EQREL_1:24

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ holds b₂ /\ (b₂ "\/" b₃) = b₂

proof end;

theorem Th25: :: EQREL_1:25

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ holds b₂ "\/" (b₂ /\ b₃) = b₂

proof end;

scheme :: EQREL_1:sch 1
s1{ F₁() -> set , P₁[ set , set ] } :

ex b₁ being Equivalence_Relation of F₁() st
for b₂, b₃ being set holds
( [b₂,b₃] in b₁ iff ( b₂ in F₁() & b₃ in F₁() & P₁[b₂,b₃] ) )

provided

E11: for b₁ being set st b₁ in F₁() holds
P₁[b₁,b₁] and
E12: for b₁, b₂ being set st P₁[b₁,b₂] holds
P₁[b₂,b₁] and
E13: for b₁, b₂, b₃ being set st P₁[b₁,b₂] & P₁[b₂,b₃] holds
P₁[b₁,b₃]

proof end;

definition

let c₁ be set ;
let c₂ be Tolerance of c₁;
let c₃ be set ;
func Class c₂,c₃ -> Subset of a₁ equals :: EQREL_1:def 4
a₂ .: {a₃};
correctness ;

end;

:: deftheorem Def4 defines Class EQREL_1:def 4 :

theorem Th26: :: EQREL_1:26

canceled;

theorem Th27: :: EQREL_1:27

for b₁, b₂, b₃ being set
for b₄ being Tolerance of b₁ holds
( b₂ in Class b₄,b₃ iff [b₂,b₃] in b₄ )

proof end;

theorem Th28: :: EQREL_1:28

for b₁ being set
for b₂ being Tolerance of b₁
for b₃ being set st b₃ in b₁ holds
b₃ in Class b₂,b₃

proof end;

theorem Th29: :: EQREL_1:29

for b₁ being set
for b₂ being Tolerance of b₁
for b₃ being set st b₃ in b₁ holds
ex b₄ being set st b₃ in Class b₂,b₄

proof end;

theorem Th30: :: EQREL_1:30

for b₁, b₂, b₃, b₄ being set
for b₅ being transitive Tolerance of b₁ st b₂ in Class b₅,b₃ & b₄ in Class b₅,b₃ holds
[b₂,b₄] in b₅

proof end;

Lemma13: for b₁, b₂ being set
for b₃ being Equivalence_Relation of b₁
for b₄ being set st b₄ in b₁ holds
( [b₄,b₂] in b₃ iff Class b₃,b₄ = Class b₃,b₂ )

proof end;

theorem Th31: :: EQREL_1:31

for b₁, b₂ being set
for b₃ being Equivalence_Relation of b₁
for b₄ being set st b₄ in b₁ holds
( b₂ in Class b₃,b₄ iff Class b₃,b₄ = Class b₃,b₂ )

proof end;

theorem Th32: :: EQREL_1:32

for b₁ being set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ & not Class b₂,b₃ = Class b₂,b₄ holds
Class b₂,b₃ misses Class b₂,b₄

proof end;

theorem Th33: :: EQREL_1:33

for b₁, b₂ being set st b₂ in b₁ holds
Class (id b₁),b₂ = {b₂}

proof end;

theorem Th34: :: EQREL_1:34

for b₁, b₂ being set st b₂ in b₁ holds
Class (nabla b₁),b₂ = b₁

proof end;

theorem Th35: :: EQREL_1:35

for b₁ being set
for b₂ being Equivalence_Relation of b₁ st ex b₃ being set st Class b₂,b₃ = b₁ holds
b₂ = nabla b₁

proof end;

theorem Th36: :: EQREL_1:36

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

proof end;

theorem Th37: :: EQREL_1:37

for b₁ being set
for b₂, b₃, b₄ being Equivalence_Relation of b₁ st b₄ = b₂ \/ b₃ holds
for b₅ being set holds
( not b₅ in b₁ or Class b₄,b₅ = Class b₂,b₅ or Class b₄,b₅ = Class b₃,b₅ )

proof end;

theorem Th38: :: EQREL_1:38

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ holds
( not b₂ \/ b₃ = nabla b₁ or b₂ = nabla b₁ or b₃ = nabla b₁ )

proof end;

definition

let c₁ be set ;
let c₂ be Equivalence_Relation of c₁;
func Class c₂ -> Subset-Family of a₁ means :Def5: :: EQREL_1:def 5
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being set st
( b₂ in a₁ & b₁ = Class a₂,b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Class EQREL_1:def 5 :

theorem Th39: :: EQREL_1:39

canceled;

theorem Th40: :: EQREL_1:40

for b₁ being set
for b₂ being Equivalence_Relation of b₁ st b₁ = {} holds
Class b₂ = {}

proof end;

definition

let c₁ be set ;
mode a_partition of c₁ -> Subset-Family of a₁ means :Def6: :: EQREL_1:def 6
( union a₂ = a₁ & ( for b₁ being Subset of a₁ st b₁ in a₂ holds
( b₁ <> {} & ( for b₂ being Subset of a₁ holds
( not b₂ in a₂ or b₁ = b₂ or b₁ misses b₂ ) ) ) ) ) if a₁ <> {}
otherwise a₂ = {} ;
existence

proof end;

consistency ;

end;

:: deftheorem Def6 defines a_partition EQREL_1:def 6 :

theorem Th41: :: EQREL_1:41

canceled;

theorem Th42: :: EQREL_1:42

for b₁ being set
for b₂ being Equivalence_Relation of b₁ holds Class b₂ is a_partition of b₁

proof end;

theorem Th43: :: EQREL_1:43

for b₁ being set
for b₂ being a_partition of b₁ ex b₃ being Equivalence_Relation of b₁ st b₂ = Class b₃

proof end;

theorem Th44: :: EQREL_1:44

for b₁, b₂ being set
for b₃ being Equivalence_Relation of b₁
for b₄ being set st b₄ in b₁ holds
( [b₄,b₂] in b₃ iff Class b₃,b₄ = Class b₃,b₂ ) by Lemma13;

theorem Th45: :: EQREL_1:45

for b₁, b₂ being set
for b₃ being Equivalence_Relation of b₂ st b₁ in Class b₃ holds
ex b₄ being Element of b₂ st b₁ = Class b₃,b₄

proof end;

registration

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

proof end;

end;

registration

let c₁ be set ;
cluster -> with_non-empty_elements a_partition of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Equivalence_Relation of c₁;
redefine func Class as Class c₂ -> a_partition of a₁;
coherence by Th42;

end;

registration

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
cluster Class a₂ -> non empty ;
coherence ;

end;

registration

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
cluster Class a₂ -> non empty with_non-empty_elements ;
coherence ;

end;