environ
vocabularies ENUMSET,RELATION,RELAT_AB,EQREL;
notations ENUMSET,RELATION,RELAT_AB;
constructors ENUMSET,RELATION,RELAT_AB;
definitions ENUMSET,RELATION,RELAT_AB;
equalities ENUMSET,RELATION,RELAT_AB;
theorems ENUMSET,RELATION,RELAT_AB;
begin
reserve A,B,X,Y,Z,V,a,b,c,d,e,x,y,z for set, P,Q,R for Relation,
S for Relation of A,A;
dom (R~) = rng R
proof
thus dom (R~) c= rng R
proof
let a;
assume a in dom (R~);
then consider b such that
b: [a,b] in R~ by RELAT_AB:def 1;
[b,a] in R by b,RELATION:def 3;
hence a in rng R by RELAT_AB:def 2;
end;
thus rng R c= dom (R~)
proof
let a;
assume a in rng R;
then consider b such that
b: [b,a] in R by RELAT_AB:def 2;
[a,b] in R~ by b,RELATION:def 3;
hence a in dom (R~) by RELAT_AB:def 1;
end;
end;
rng R = R.:dom R
proof
thus rng R c= R.:dom R
proof
let a;
assume a in rng R;
then consider b such that
b: [b,a] in R by RELAT_AB:def 2;
b in dom R by b,RELAT_AB:def 1;
hence a in R.:dom R by b,RELAT_AB:def 3;
end;
thus R.:dom R c= rng R
proof
let a;
assume a in R.:dom R;
then consider b such that
b: [b,a] in R & b in dom R by RELAT_AB:def 3;
thus a in rng R by b,RELAT_AB:def 2;
end;
end;
(P*R).:X = R.:(P.:X)
proof
thus (P*R).:X c= R.:(P.:X)
proof
let a;
assume a in (P*R).:X;
then consider b such that
b: [b,a] in P*R & b in X by RELAT_AB:def 3;
consider c such that
c: [b,c] in P & [c,a] in R by RELATION:def 7,b;
c in (P.:X) by b,c,RELAT_AB:def 3;
hence a in R.:(P.:X) by c,RELAT_AB:def 3;
end;
thus R.:(P.:X) c= (P*R).:X
proof
let a;
assume a in R.:(P.:X);
then consider b such that
b: [b,a] in R & b in P.:X by RELAT_AB:def 3;
consider c such that
c: [c,b] in P & c in X by b,RELAT_AB:def 3;
[c,a] in P*R by b,c,RELATION:def 7;
hence a in (P*R).:X by c,RELAT_AB:def 3;
end;
end;
R"(X\/Y) = (R"X) \/ (R"Y)
proof
thus R"(X\/Y) c= (R"X) \/ (R"Y)
proof
let a;
assume a in R"(X\/Y);
then consider b such that
b: [a,b] in R & b in X \/ Y by RELAT_AB:def 4;
b in X or b in Y by ENUMSET:def 6,b;
then a in R"X or a in R"Y by b,RELAT_AB:def 4;
hence a in (R"X) \/ (R"Y) by ENUMSET:def 6;
end;
thus (R"X) \/ (R"Y) c= R"(X\/Y)
proof
let a;
assume a in (R"X) \/ (R"Y);
then per cases by ENUMSET:def 6;
suppose a in R"(X);
then consider b such that
b: [a,b] in R & b in X by RELAT_AB:def 4;
b in X\/Y by b,ENUMSET:def 6;
hence a in R"(X\/Y) by b,RELAT_AB:def 4;
end;
suppose a in R"Y;
then consider b such that
b: [a,b] in R & b in Y by RELAT_AB:def 4;
b in X\/Y by b,ENUMSET:def 6;
hence a in R"(X\/Y) by b,RELAT_AB:def 4;
end;
end;
end;
definition
let X be set;
mode Equivalence_Relation of X -> Relation of X,X means :ER:
it is reflexive & it is symmetric & it is transitive;
existence
proof
take id X;
thus id X is reflexive
proof
let x;
assume x in X;
hence [x,x] in id X by RELAT_AB:def 6;
end;
thus id X is symmetric
proof
let x,y;
assume a: [x,y] in id X;
then x in X & x=y by RELAT_AB:def 6;
hence [y,x] in id X by a;
end;
thus id X is transitive
proof
let x,y,z;
assume a: [x,y] in id X & [y,z] in id X;
then x in X & x=y & y in X & y=z by RELAT_AB:def 6;
hence [x,z] in id X by a;
end;
end;
end;
definition
let X,x be set;
let R be Relation of X,X;
func EqClass(x,R) -> set equals R.:({x});
correctness;
end;
reserve R for Relation of X,X;
dom R = X & R is symmetric & R is transitive implies R is reflexive
proof
assume d: dom R = X;
assume s: R is symmetric;
assume t: R is transitive;
let x;
assume x in X;
then consider y such that y:
[x,y] in R by d,RELAT_AB:def 1;
[y,x] in R by y,s,RELATION:def 11;
hence [x,x] in R by y,t,RELATION:def 12;
end;
reserve R for Equivalence_Relation of X;
L0:
y in EqClass(x,R) iff [x,y] in R
proof
thus y in EqClass(x,R) implies [x,y] in R
proof
assume y in EqClass(x,R);
then y in R.:({x});
then consider z such that
z: [z,y] in R & z in {x} by RELAT_AB:def 3;
z=x by z,ENUMSET:def 3;
hence [x,y] in R by z;
end;
thus [x,y] in R implies y in EqClass(x,R)
proof
assume a: [x,y] in R;
x in {x} by ENUMSET:def 3;
then y in R.:({x}) by a,RELAT_AB:def 3;
hence y in EqClass(x,R);
end;
end;
x in X implies x in EqClass(x,R)
proof
assume x: x in X;
R is reflexive by ER;
then [x,x] in R by RELAT_AB:def 8,x;
hence x in EqClass(x,R) by L0;
end;
y in EqClass(x,R) implies EqClass(y,R)=EqClass(x,R)
proof
assume y in EqClass(x,R);
then y: [x,y] in R by L0;
t: R is transitive by ER;
s: R is symmetric by ER;
thus EqClass(y,R) c= EqClass(x,R)
proof
let a;
assume a in EqClass(y,R);
then [y,a] in R by L0;
then [x,a] in R by y,t,RELATION:def 12;
hence a in EqClass(x,R) by L0;
end;
thus EqClass(x,R) c= EqClass(y,R)
proof
let a;
assume a in EqClass(x,R);
then [x,a] in R by L0;
then [a,x] in R by s,RELATION:def 11;
then [a,y] in R by y,t,RELATION:def 12;
then [y,a] in R by s,RELATION:def 11;
hence a in EqClass(y,R) by L0;
end;
end;
EqClass(x,R) meets EqClass(y,R) implies EqClass(x,R) = EqClass(y,R)
proof
s: R is symmetric by ER;
t: R is transitive by ER;
assume EqClass(x,R) meets EqClass(y,R);
then EqClass(x,R) /\ EqClass(y,R) <> {} by ENUMSET:def 12;
then consider b such that
b: b in EqClass(x,R) /\ EqClass(y,R) by ENUMSET:def 1;
b in EqClass(x,R) & b in EqClass(y,R) by b,ENUMSET:def 7;
then bb: [x,b] in R & [y,b] in R by L0;
thus EqClass(x,R) c= EqClass(y,R)
proof
let a;
assume a in EqClass(x,R);
then [x,a] in R by L0;
then [a,x] in R by s,RELATION:def 11;
then [a,b] in R by bb,t,RELATION:def 12;
then [b,a] in R by s,RELATION:def 11;
then [y,a] in R by bb,t,RELATION:def 12;
hence a in EqClass(y,R) by L0;
end;
thus EqClass(y,R) c= EqClass(x,R)
proof
let a;
assume a in EqClass(y,R);
then [y,a] in R by L0;
then [a,y] in R by s,RELATION:def 11;
then [a,b] in R by bb,t,RELATION:def 12;
then [b,a] in R by s,RELATION:def 11;
then [x,a] in R by bb,t,RELATION:def 12;
hence a in EqClass(x,R) by L0;
end;
end;
for A st (for B holds B in A iff ex x st B=EqClass(x,R) & x in X)
holds union A = X
proof
let A;
assume b: for B holds B in A iff ex x st B=EqClass(x,R) & x in X;
thus union A c= X
proof
let a;
assume a in union A;
then consider B such that
B: a in B & B in A by ENUMSET:def 13;
consider x such that
x: B=EqClass(x,R) & x in X by b,B;
[x,a] in R by L0,x,B;
then r: a in rng R by RELAT_AB:def 2;
rng R c= X by RELAT_AB:def 5;
hence a in X by r,ENUMSET:def 10;
end;
thus X c= union A
proof
let a;
r: R is reflexive by ER;
assume a: a in X;
then [a,a] in R by r,RELAT_AB:def 8;
then ae: a in EqClass(a,R) by L0;
EqClass(a,R) in A by a,b;
hence a in union A by ae,ENUMSET:def 13;
end;
end;
definition
let X;
mode Partition of X -> set means
(for A st A in it holds A c= X & A <> {}) &
(for A,B st A in it & B in it holds A misses B or A=B) &
union it = X;
existence
proof
per cases;
suppose X: X = {};
take {};
thus for A st A in {} holds A c= X & A <> {} by ENUMSET:def 1;
thus for A,B st A in {} & B in {} holds A misses B or A=B by ENUMSET:def 1;
thus union {} = X
proof
thus union {} c= X
proof
let a;
assume a in union {};
then ex b st a in b & b in {} by ENUMSET:def 13;
hence thesis by ENUMSET:def 1;
end;
thus X c= union {}
proof
let a;
assume a in X;
hence thesis by X,ENUMSET:def 1;
end;
end;
end;
suppose X: X <> {};
take {X};
thus for A st A in {X} holds A c= X & A <> {}
proof
let A;
assume A in {X};
then a: A = X by ENUMSET:def 3;
thus A c= X
proof
let a;
assume a in A;
hence a in X by a;
end;
thus A <> {} by X,a;
end;
thus for A,B st A in {X} & B in {X} holds A misses B or A=B
proof
let A,B;
assume A in {X} & B in {X};
then A = X & B = X by ENUMSET:def 3;
hence thesis;
end;
thus union {X} = X
proof
thus union {X} c= X
proof
let a;
assume a in union {X};
then consider b such that
b: a in b & b in {X} by ENUMSET:def 13;
b = X by b,ENUMSET:def 3;
hence a in X by b;
end;
thus X c= union {X}
proof
let a;
assume x: a in X;
X in {X} by ENUMSET:def 3;
hence a in union {X} by x,ENUMSET:def 13;
end;
end;
end;
end;
end;