:: EQREL_1 semantic presentation

definition

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

end;

:: deftheorem defines nabla EQREL_1:def 1 :

registration

let X be set ;
cluster nabla X -> reflexive total ;
coherence

proof end;

end;

definition

let X be set ;
let R1, R2 be Relation of X;
:: original: /\
redefine func R1 /\ R2 -> Relation of X;
coherence

proof end;

:: original: \/
redefine func R1 \/ R2 -> Relation of X;
coherence

proof end;

end;

Lm1: for i, j being Nat st i < j holds
j - i is Nat
by NAT_1:61;

theorem :: EQREL_1:1

canceled;

theorem :: EQREL_1:2

canceled;

theorem :: EQREL_1:3

canceled;

theorem :: EQREL_1:4

for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )

proof end;

definition

let X be set ;
mode Tolerance of X is reflexive symmetric total Relation of X;
mode Equivalence_Relation of X is symmetric transitive total Relation of X;

end;

theorem :: EQREL_1:5

canceled;

theorem :: EQREL_1:6

for X being set holds id X is Equivalence_Relation of X ;

theorem Th7: :: EQREL_1:7

for X being set holds nabla X is Equivalence_Relation of X

proof end;

registration

let X be set ;
cluster nabla X -> reflexive symmetric transitive total ;
coherence by Th7;

end;

Lm2: for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )

proof end;

theorem :: EQREL_1:8

canceled;

theorem :: EQREL_1:9

canceled;

theorem :: EQREL_1:10

canceled;

theorem Th11: :: EQREL_1:11

for X, x being set
for R being reflexive total Relation of X st x in X holds
[x,x] in R

proof end;

theorem Th12: :: EQREL_1:12

for X, x, y being set
for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R

proof end;

theorem Th13: :: EQREL_1:13

for X, x, y, z being set
for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R

proof end;

theorem :: EQREL_1:14

for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} by Th11;

theorem :: EQREL_1:15

canceled;

theorem Th16: :: EQREL_1:16

for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )

proof end;

definition

let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
:: original: /\
redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
coherence

proof end;

end;

theorem :: EQREL_1:17

for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X

proof end;

theorem :: EQREL_1:18

for X being set
for R being Relation of X holds (nabla X) /\ R = R by XBOOLE_1:28;

theorem Th19: :: EQREL_1:19

for X being set
for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X

proof end;

theorem Th20: :: EQREL_1:20

for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )

proof end;

definition

let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
canceled;
func EqR1 "\/" EqR2 -> Equivalence_Relation of X means :Def3: :: EQREL_1:def 3
( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
it c= EqR ) );
existence by Th20;
uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem EQREL_1:def 2 :

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

theorem :: EQREL_1:21

canceled;

theorem :: EQREL_1:22

for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;

theorem :: EQREL_1:23

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqR2 "\/" EqR1 ;

theorem :: EQREL_1:24

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1

proof end;

theorem :: EQREL_1:25

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1

proof end;

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

ex EqR being Equivalence_Relation of F₁() st
for x, y being set holds
( [x,y] in EqR iff ( x in F₁() & y in F₁() & P₁[x,y] ) )

provided

A1: for x being set st x in F₁() holds
P₁[x,x] and
A2: for x, y being set st P₁[x,y] holds
P₁[y,x] and
A3: for x, y, z being set st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;

definition

let X be set ;
let R be Tolerance of X;
let x be set ;
func Class R,x -> Subset of X equals :: EQREL_1:def 4
R .: {x};
correctness ;

end;

:: deftheorem defines Class EQREL_1:def 4 :

theorem :: EQREL_1:26

canceled;

theorem Th27: :: EQREL_1:27

for X, y, x being set
for R being Tolerance of X holds
( y in Class R,x iff [y,x] in R )

proof end;

theorem Th28: :: EQREL_1:28

for X being set
for R being Tolerance of X
for x being set st x in X holds
x in Class R,x

proof end;

theorem :: EQREL_1:29

for X being set
for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class R,y

proof end;

theorem :: EQREL_1:30

for X, y, x, z being set
for R being transitive Tolerance of X st y in Class R,x & z in Class R,x holds
[y,z] in R

proof end;

Lm3: for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class EqR,x = Class EqR,y )

proof end;

theorem Th31: :: EQREL_1:31

for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class EqR,x iff Class EqR,x = Class EqR,y )

proof end;

theorem Th32: :: EQREL_1:32

for X being set
for EqR being Equivalence_Relation of X
for x, y being set st x in X & y in X & not Class EqR,x = Class EqR,y holds
Class EqR,x misses Class EqR,y

proof end;

theorem :: EQREL_1:33

for X, x being set st x in X holds
Class (id X),x = {x}

proof end;

theorem Th34: :: EQREL_1:34

for X, x being set st x in X holds
Class (nabla X),x = X

proof end;

theorem Th35: :: EQREL_1:35

for X being set
for EqR being Equivalence_Relation of X st ex x being set st Class EqR,x = X holds
EqR = nabla X

proof end;

theorem :: EQREL_1:36

for x, X, y being set
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )

proof end;

theorem Th37: :: EQREL_1:37

for X being set
for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class E,x = Class EqR1,x or Class E,x = Class EqR2,x )

proof end;

theorem :: EQREL_1:38

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )

proof end;

definition

let X be set ;
let EqR be Equivalence_Relation of X;
func Class EqR -> Subset-Family of X means :Def5: :: EQREL_1:def 5
for A being Subset of X holds
( A in it iff ex x being set st
( x in X & A = Class EqR,x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Class EQREL_1:def 5 :

theorem :: EQREL_1:39

canceled;

theorem Th40: :: EQREL_1:40

for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}

proof end;

definition

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

proof end;

consistency ;

end;

:: deftheorem Def6 defines a_partition EQREL_1:def 6 :

theorem :: EQREL_1:41

canceled;

theorem Th42: :: EQREL_1:42

for X being set
for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X

proof end;

theorem :: EQREL_1:43

for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR

proof end;

theorem :: EQREL_1:44

for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class EqR,x = Class EqR,y ) by Lm3;

theorem :: EQREL_1:45

for x, X being set
for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class EqR,y

proof end;

registration

let X be non empty set ;
cluster -> non empty a_partition of X;
coherence

proof end;

end;

registration

let X be set ;
cluster -> with_non-empty_elements a_partition of X;
coherence

proof end;

end;

definition

let X be set ;
let R be Equivalence_Relation of X;
:: original: Class
redefine func Class R -> a_partition of X;
coherence by Th42;

end;

registration

let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> non empty ;
coherence ;

end;

registration

let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> non empty with_non-empty_elements ;
coherence ;

end;