:: Equivalence Relations and Classes of Abstraction
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ZFMISC_1, SETFAM_1, TARSKI, PARTFUN1,
RELAT_2, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1, ARYTM_3, ORDINAL4,
ARYTM_1, NAT_1, CARD_1, EQREL_1, MCART_1, CARD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, DOMAIN_1, SUBSET_1,
XCMPLX_0, XXREAL_0, RELAT_1, RELAT_2, SETFAM_1, FINSEQ_1, FUNCT_1,
ORDINAL1, NUMBERS, NAT_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1;
constructors SETFAM_1, RELAT_2, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
RELSET_1, FUNCT_3, BINOP_1, DOMAIN_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1,
RELAT_1, ORDINAL1, RELSET_1, FUNCT_2, ZFMISC_1, FUNCT_1, RELAT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_1, RELAT_2, XBOOLE_0, PARTFUN1, SETFAM_1;
equalities TARSKI, RELAT_1, SUBSET_1, BINOP_1;
expansions TARSKI, RELAT_1, RELAT_2, XBOOLE_0;
theorems RELAT_1, RELAT_2, RELSET_1, SETFAM_1, ZFMISC_1, TARSKI, FINSEQ_1,
NAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1, PARTFUN1, XREAL_1, XXREAL_0,
FUNCT_1, FUNCT_3, FUNCT_2, MCART_1, SUBSET_1, SETWISEO, XTUPLE_0;
schemes SUBSET_1, RELSET_1, FINSEQ_1, NAT_1, FUNCT_2;
begin
reserve X,Y,Z for set, x,y,z for object;
reserve i,j for Nat;
reserve A,B,C for Subset of X;
reserve R,R1,R2 for Relation of X;
reserve AX for Subset of [:X,X:];
reserve SFXX for Subset-Family of [:X,X:];
:: Equivalence Relation and its properties
definition
let X;
func nabla X -> Relation of X equals
[:X,X:];
coherence
proof
[:X,X:] c=[:X,X:];
hence thesis;
end;
end;
registration
let X;
cluster nabla X -> total reflexive;
coherence
proof
thus dom nabla X c= X;
thus X c= dom nabla X
proof
let x be object;
assume x in X;
then [x,x] in [:X,X:] by ZFMISC_1:87;
hence thesis by XTUPLE_0:def 12;
end;
let x be object;
assume x in field nabla X;
then x in dom nabla X \/ rng nabla X;
hence thesis by ZFMISC_1:87;
end;
end;
definition
let X,R1,R2;
redefine func R1 /\ R2 -> Relation of X; :: redefines /\ (XBOOLE_0, definition)
coherence
proof
R1 /\ R2 c= [:X,X:];
hence thesis;
end;
redefine func R1 \/ R2 -> Relation of X; :: redefines \/ (XBOOLE_0, definition)
coherence
proof
R1 \/ R2 c= [:X,X:];
hence thesis;
end;
end;
theorem
nabla X \/ R1 = nabla X by XBOOLE_1:12;
theorem
id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X
by RELAT_1:def 10;
definition
let X;
mode Tolerance of X is total reflexive symmetric Relation of X;
mode Equivalence_Relation of X is total symmetric transitive Relation of X;
end;
theorem
id X is Equivalence_Relation of X;
theorem Th4:
nabla X is Equivalence_Relation of X
proof
for x,y holds x in X & y in X & [x,y] in nabla X implies [y,x] in nabla
X by ZFMISC_1:88;
then
A1: nabla X is_symmetric_in X;
for x,y,z st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in
nabla X holds [x,z] in nabla X by ZFMISC_1:87;
then
A2: nabla X is_transitive_in X;
field nabla X = X by ORDERS_1:12;
hence thesis by A1,A2,RELAT_2:def 11,def 16;
end;
registration
let X;
cluster nabla X -> total symmetric transitive;
coherence by Th4;
end;
reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;
Lm1: [x,y] in R implies x in X & y in X
proof
assume [x,y] in R;
then x in dom R & y in rng R by XTUPLE_0:def 12,def 13;
hence thesis;
end;
theorem Th5:
for R being total reflexive Relation of X holds x in X implies [x,x] in R
proof
let R be total reflexive Relation of X;
field R = X by ORDERS_1:12;
then R is_reflexive_in X by RELAT_2:def 9;
hence thesis;
end;
theorem Th6:
for X being set, x,y being object, R being symmetric Relation of X
st [x,y] in R holds [y,x] in R
proof
let X be set, x,y be object, R be symmetric Relation of X;
assume A1: [x,y] in R;
then x in field R & y in field R by RELAT_1:15;
hence thesis by A1, RELAT_2:def 3, RELAT_2:def 11;
end;
theorem Th7:
for R being total transitive Relation of X
for x,y being object
holds [x,y] in R & [y,z] in R implies [x,z] in R
proof
let R be total transitive Relation of X;
let x,y be object;
assume that
A1: [x,y] in R and
A2: [y,z] in R;
A3: z in X by A2,Lm1;
field R = X by ORDERS_1:12;
then
A4: R is_transitive_in X by RELAT_2:def 16;
x in X & y in X by A1,Lm1;
hence thesis by A1,A2,A3,A4;
end;
theorem
for R being total reflexive Relation of X holds
(ex x being set st x in X) implies R <> {};
theorem Th9:
R is Equivalence_Relation of X iff
R is reflexive symmetric transitive & field R = X
by ORDERS_1:12,ORDERS_1:13,PARTFUN1:def 2;
definition
let X,EqR1,EqR2;
redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X; :: redefines /\ (XBOOLE_0, definition)
coherence
proof
for x being object st x in X holds [x,x] in EqR2 by Th5;
then
A1: id X c= EqR2 by RELAT_1:47;
for x being object st x in X holds [x,x] in EqR1 by Th5;
then id X c= EqR1 by RELAT_1:47;
then id X c= EqR1 /\ EqR2 by A1,XBOOLE_1:19;
then dom(EqR1 /\ EqR2) = X & rng(EqR1 /\ EqR2) = X by RELSET_1:16;
then field (EqR1 /\ EqR2) = X;
hence thesis by Th9;
end;
end;
theorem
id X /\ EqR = id X
proof
now
let x,y be object;
assume [x,y] in id X;
then x in X & x = y by RELAT_1:def 10;
hence [x,y] in EqR by Th5;
end;
then id X c= EqR;
hence thesis by XBOOLE_1:28;
end;
theorem Th11:
for SFXX st (SFXX <> {} & for Y st Y in SFXX holds Y is
Equivalence_Relation of X) holds meet SFXX is Equivalence_Relation of X
proof
let SFXX such that
A1: SFXX <> {} and
A2: for Y st Y in SFXX holds Y is Equivalence_Relation of X;
reconsider XX = meet SFXX as Relation of X;
A3: XX is_symmetric_in X
proof
let x,y;
assume that
x in X and
y in X and
A4: [x,y] in XX;
now
let Y;
assume Y in SFXX;
then Y is Equivalence_Relation of X & [x,y] in Y by A2,A4,SETFAM_1:def 1;
hence [y,x] in Y by Th6;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
A5: XX is_transitive_in X
proof
let x,y,z;
assume that
x in X and
y in X and
z in X and
A6: [x,y] in XX and
A7: [y,z] in XX;
now
let Y;
assume
A8: Y in SFXX;
then
A9: [y,z] in Y by A7,SETFAM_1:def 1;
Y is Equivalence_Relation of X & [x,y] in Y by A2,A6,A8,SETFAM_1:def 1;
hence [x,z] in Y by A9,Th7;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
XX is_reflexive_in X
proof
let x such that
A10: x in X;
for Y st Y in SFXX holds [x,x] in Y
proof
let Y;
assume Y in SFXX;
then Y is Equivalence_Relation of X by A2;
hence thesis by A10,Th5;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
then field XX = X & dom XX = X by ORDERS_1:13;
hence thesis by A3,A5,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
theorem Th12:
for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2
proof
let R;
defpred P[set] means $1 is Equivalence_Relation of X & R c= $1;
consider F being Subset-Family of [:X,X:] such that
A1: for AX holds AX in F iff P[AX] from SUBSET_1:sch 3;
R c= nabla X;
then
A2: F <> {} by A1;
for Y st Y in F holds Y is Equivalence_Relation of X by A1;
then reconsider EqR = meet F as Equivalence_Relation of X by A2,Th11;
A3: for EqR2 st R c= EqR2 holds EqR c= EqR2 by A1,SETFAM_1:3;
take EqR;
for Y st Y in F holds R c= Y by A1;
hence thesis by A2,A3,SETFAM_1:5;
end;
definition
let X;
let EqR1,EqR2;
func EqR1 "\/" EqR2 -> Equivalence_Relation of X means
:Def2:
EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR;
existence by Th12;
uniqueness;
commutativity;
idempotence;
end;
theorem
(EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
for EqR4 be Equivalence_Relation of X holds EqR4 = EqR1 "\/" (EqR2 "\/"
EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
proof
let EqR4 be Equivalence_Relation of X;
A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3);
then
A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;
EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then EqR2 "\/" EqR3 c= EqR4 by A2;
then
A3: EqR2 \/ EqR3 c= EqR4 by A1;
EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then
A4: EqR2 c= EqR4 by A3;
EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then EqR1 c= EqR4 by A2;
then EqR1 \/ EqR2 c= EqR4 by A4,XBOOLE_1:8;
then
A5: EqR1 "\/" EqR2 c= EqR4 by Def2;
EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then EqR3 c= EqR4 by A3;
then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5,XBOOLE_1:8;
hence thesis by Def2;
end;
then
A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3);
for EqR4 be Equivalence_Relation of X holds EqR4 = (EqR1 "\/" EqR2) "\/"
EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
proof
let EqR4 be Equivalence_Relation of X;
A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3;
then
A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;
EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then EqR1 "\/" EqR2 c= EqR4 by A8;
then
A9: EqR1 \/ EqR2 c= EqR4 by A7;
EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then
A10: EqR3 c= EqR4 by A8;
EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then EqR2 c= EqR4 by A9;
then EqR2 \/ EqR3 c= EqR4 by A10,XBOOLE_1:8;
then
A11: EqR2 "\/" EqR3 c= EqR4 by Def2;
EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then EqR1 c= EqR4 by A9;
then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11,XBOOLE_1:8;
hence thesis by Def2;
end;
then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3;
hence thesis by A6;
end;
theorem
EqR "\/" EqR = EqR;
theorem
EqR1 "\/" EqR2 = EqR2 "\/" EqR1;
theorem
EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proof
thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17;
EqR1 c= EqR1 \/ EqR2 & EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2,XBOOLE_1:7;
then EqR1 c= EqR1 "\/" EqR2;
hence thesis by XBOOLE_1:19;
end;
theorem
EqR1 "\/" (EqR1 /\ EqR2) = EqR1
proof
EqR1 = EqR1 \/ (EqR1 /\ EqR2) & for EqR st EqR1 \/ (EqR1 /\ EqR2) c= EqR
holds EqR1 c= EqR by XBOOLE_1:22;
hence thesis by Def2;
end;
scheme
ExEqRel {X() -> set,P[object,object]}:
ex EqR being Equivalence_Relation of X() st
for x,y holds [x,y] in EqR iff x in X() & y in X() & P[x,y]
provided
A1: for x st x in X() holds P[x,x] and
A2: for x,y st P[x,y] holds P[y,x] and
A3: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof
consider Y being Relation of X(),X() such that
A4: for x,y holds [x,y] in Y iff x in X() & y in X() & P[x,y] from
RELSET_1:sch 1;
A5: Y is_transitive_in X()
proof
let x,y,z;
assume that
A6: x in X() and
y in X() and
A7: z in X() and
A8: [x,y] in Y & [y,z] in Y;
( P[x,y])& P[y,z] by A4,A8;
then P[x,z] by A3;
hence thesis by A4,A6,A7;
end;
A9: Y is_symmetric_in X()
proof
let x,y;
assume that
A10: x in X() & y in X() and
A11: [x,y] in Y;
P[x,y] by A4,A11;
then P[y,x] by A2;
hence thesis by A4,A10;
end;
Y is_reflexive_in X()
by A1,A4;
then field Y = X() & dom Y = X() by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of X() by A9,A5,PARTFUN1:def 2
,RELAT_2:def 11,def 16;
take R1;
thus thesis by A4;
end;
:: Classes of abstraction
notation
let R be Relation, x be object;
synonym Class(R,x) for Im(R,x);
end;
definition
let X, Y be set, R be Relation of X, Y, x be object;
redefine func Class(R,x) -> Subset of Y; :: redefines Class (EQREL_1, synonym) → Im (RELAT_1, definition)
coherence
proof
R.:{x} c= Y;
hence thesis;
end;
end;
theorem
for R being Relation holds y in Class (R,x) iff [x,y] in R
proof
let R be Relation;
thus y in Class(R,x) implies [x,y] in R
proof
assume y in Class(R,x);
then ex z being object st [z,y] in R & z in {x} by RELAT_1:def 13;
hence thesis by TARSKI:def 1;
end;
A1: x in {x} by TARSKI:def 1;
assume [x,y] in R;
hence thesis by A1,RELAT_1:def 13;
end;
theorem Th19:
for R being total symmetric Relation of X holds y in Class (R,x)
iff [y,x] in R
proof
let R be total symmetric Relation of X;
thus y in Class(R,x) implies [y,x] in R
proof
assume y in Class(R,x);
then ex z being object st [z,y] in R & z in {x} by RELAT_1:def 13;
then [x,y] in R by TARSKI:def 1;
hence thesis by Th6;
end;
assume [y,x] in R;
then
A1: [x,y] in R by Th6;
x in {x} by TARSKI:def 1;
hence thesis by A1,RELAT_1:def 13;
end;
theorem Th20:
for R being Tolerance of X holds for x st x in X holds x in Class (R,x)
proof
let R be Tolerance of X;
let x;
assume x in X;
then [x,x] in R by Th5;
hence thesis by Th19;
end;
theorem
for R being Tolerance of X holds for x st x in X holds
ex y st x in Class(R,y)
proof
let R be Tolerance of X;
let x;
assume x in X;
then x in Class(R,x) by Th20;
hence thesis;
end;
theorem
for R being transitive Tolerance of X holds y in Class(R,x) & z in
Class(R,x) implies [y,z] in R
proof
let R be transitive Tolerance of X;
assume that
A1: y in Class(R,x) and
A2: z in Class(R,x);
[z,x] in R by A2,Th19;
then
A3: [x,z] in R by Th6;
[y,x] in R by A1,Th19;
hence thesis by A3,Th7;
end;
Lm2: for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y)
proof
let x such that
A1: x in X;
thus [x,y] in EqR implies Class(EqR,x) = Class(EqR,y)
proof
assume
A2: [x,y] in EqR;
now
let z be object;
assume z in Class(EqR,y);
then
A3: [z,y] in EqR by Th19;
[y,x] in EqR by A2,Th6;
then [z,x] in EqR by A3,Th7;
hence z in Class(EqR,x) by Th19;
end;
then
A4: Class(EqR,y) c= Class(EqR,x);
now
let z be object;
assume z in Class(EqR,x);
then [z,x] in EqR by Th19;
then [z,y] in EqR by A2,Th7;
hence z in Class(EqR,y) by Th19;
end;
then Class(EqR,x) c= Class(EqR,y);
hence thesis by A4;
end;
assume Class(EqR,x) = Class(EqR,y);
then x in Class(EqR,y) by A1,Th20;
hence thesis by Th19;
end;
theorem Th23:
for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class (EqR,y)
proof
let x such that
A1: x in X;
thus y in Class(EqR,x) implies Class(EqR,x) = Class(EqR,y)
proof
assume y in Class(EqR,x);
then [y,x] in EqR by Th19;
then [x,y] in EqR by Th6;
hence thesis by A1,Lm2;
end;
assume Class(EqR,x) = Class(EqR,y);
then [x,y] in EqR by A1,Lm2;
then [y,x] in EqR by Th6;
hence thesis by Th19;
end;
theorem Th24:
for x,y st y in X holds
Class(EqR,x) = Class(EqR,y) or Class(EqR,x) misses Class(EqR,y)
proof
let x,y;
A1: not [x,y] in EqR implies Class(EqR,x) misses Class(EqR,y)
proof
assume
A2: not [x,y] in EqR;
assume Class(EqR,x) meets Class(EqR,y);
then consider z being object such that
A3: z in Class(EqR,x) and
A4: z in Class(EqR,y) by XBOOLE_0:3;
[z,x] in EqR by A3,Th19;
then
A5: [x,z] in EqR by Th6;
[z,y] in EqR by A4,Th19;
hence contradiction by A2,A5,Th7;
end;
assume
A6: y in X;
[x,y] in EqR implies Class(EqR,x) = Class(EqR,y)
proof
assume [x,y] in EqR;
then x in Class(EqR,y) by Th19;
hence thesis by A6,Th23;
end;
hence thesis by A1;
end;
theorem Th25:
for x st x in X holds Class(id X,x) = {x}
proof
let x;
A1: now
let y;
assume y in Class(id X,x);
then [y,x] in id X by Th19;
hence y = x by RELAT_1:def 10;
end;
assume x in X;
then for y being object holds y in Class(id X,x) iff y = x by A1,Th20;
hence thesis by TARSKI:def 1;
end;
theorem Th26:
for x st x in X holds Class(nabla X,x) = X
proof
let x such that
A1: x in X;
now
let y be object;
assume y in X;
then [y,x] in nabla X by A1,ZFMISC_1:87;
hence y in Class(nabla X,x) by Th19;
end;
then for y being object holds y in X iff y in Class(nabla X,x);
hence thesis by TARSKI:2;
end;
theorem Th27:
(ex x st Class(EqR,x) = X) implies EqR = nabla X
proof
given x such that
A1: Class(EqR,x) = X;
[:X,X:] c= EqR
proof
let y,z be object;
assume
A2: [y,z] in [:X,X:];
then z in Class(EqR,x) by A1,ZFMISC_1:87;
then [z,x] in EqR by Th19;
then
A3: [x,z] in EqR by Th6;
y in Class(EqR,x) by A1,A2,ZFMISC_1:87;
then [y,x] in EqR by Th19;
hence thesis by A3,Th7;
end;
hence thesis;
end;
theorem
x in X implies ([x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f
.(i+1)] in EqR1 \/ EqR2)
proof
assume
A1: x in X;
thus [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st 1 <= len f &
x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in
EqR1 \/ EqR2
proof
defpred P[object,object] means
ex f being FinSequence st (1 <= len f & $1 = f.1
& $2 = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/
EqR2);
consider Y being Relation of X,X such that
A2: for x,y holds [x,y] in Y iff x in X & y in X & P[x,y] from
RELSET_1:sch 1;
A3: Y is_transitive_in X
proof
let x,y,z;
assume that
A4: x in X and
A5: y in X and
A6: z in X and
A7: [x,y] in Y and
A8: [y,z] in Y;
consider g being FinSequence such that
A9: 1 <= len g and
A10: y = g.1 and
A11: z = g.(len g) and
A12: for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 by A2,A8;
consider f being FinSequence such that
A13: 1 <= len f and
A14: x = f.1 and
A15: y = f.(len f) and
A16: for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 by A2,A7;
set h = f^g;
A17: len h = len f + len g by FINSEQ_1:22;
A18: len f + 1 <= len f + len g by A9,XREAL_1:7;
then
A19: h.(len h) = g.(len g + len f - len f) by A17,FINSEQ_1:23
.= g.(len g);
A20: for i st 1 <= i & i < len h holds [h.i,h.(i+1)] in EqR1 \/ EqR2
proof
let i;
assume that
A21: 1 <= i and
A22: i < len h;
A23: 1 <= i & i < len f or i = len f or len f < i by A21,XXREAL_0:1;
now
per cases by A22,A23,NAT_1:13;
suppose
A24: 1 <= i & i < len f;
then 1 <= i + 1 & i + 1 <= len f by NAT_1:13;
then i + 1 in Seg len f by FINSEQ_1:1;
then i + 1 in dom f by FINSEQ_1:def 3;
then
A25: h.(i + 1) = f.(i + 1) by FINSEQ_1:def 7;
i in Seg(len f) by A24,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then h.i = f.i by FINSEQ_1:def 7;
hence thesis by A16,A24,A25;
end;
suppose
A26: i = len f;
len f in Seg len f by A13,FINSEQ_1:1;
then len f in dom f by FINSEQ_1:def 3;
then
A27: h.i = y by A15,A26,FINSEQ_1:def 7;
A28: [y,y] in EqR1 by A5,Th5;
h.(i + 1) = g.(1 + len f - len f) by A18,A26,FINSEQ_1:23
.= y by A10;
hence thesis by A27,A28,XBOOLE_0:def 3;
end;
suppose
A29: len f + 1 <= i & i < len h;
then len f < i by NAT_1:13;
then reconsider k = i - len f as Element of NAT by NAT_1:21;
i < len f + len g by A29,FINSEQ_1:22;
then
A30: i - len f < len g by XREAL_1:19;
len f + 1 <= i + 1 & i + 1 <= len f + len g by A17,A29,NAT_1:13;
then
A31: h.(i + 1) = g.(1 + i - len f) by FINSEQ_1:23
.= g.((i - len f) + 1);
1 + len f - len f <= i - len f by A29,XREAL_1:9;
then [g.k,g.(k + 1)] in EqR1 \/ EqR2 by A12,A30;
hence thesis by A17,A29,A31,FINSEQ_1:23;
end;
end;
hence thesis;
end;
1 in Seg(len f) by A13,FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def 3;
then
A32: x = h.1 by A14,FINSEQ_1:def 7;
1 <= len h by A13,A17,NAT_1:12;
hence thesis by A2,A4,A6,A11,A32,A19,A20;
end;
A33: Y is_symmetric_in X
proof
let x,y;
assume that
A34: x in X & y in X and
A35: [x,y] in Y;
consider f being FinSequence such that
A36: 1 <= len f and
A37: x = f.1 and
A38: y = f.(len f) and
A39: for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2
by A2,A35;
defpred P[Nat,object] means $2 = f.(1 + (len f) - $1);
A40: for k be Nat st k in Seg(len f) ex z being object st P[k,z];
consider g being FinSequence such that
A41: dom g = Seg(len f) & for k being Nat st k in Seg(len f) holds P
[k,g.k] from FINSEQ_1:sch 1(A40);
A42: len f = len g by A41,FINSEQ_1:def 3;
A43: for j st 1 <= j & j < len g holds [g.j,g.(j+1)] in EqR1 \/ EqR2
proof
let j;
assume that
A44: 1 <= j and
A45: j < len g;
reconsider k = (len f) - j as Element of NAT by A42,A45,NAT_1:21;
j - (len f) < (len f) - (len f) by A42,A45,XREAL_1:9;
then - ((len f) - j) < - 0;
then 0 < k;
then
A46: 0 + 1 <= k by NAT_1:13;
- j < -0 by A44,XREAL_1:24;
then (len f) + -j < 0 + (len f) by XREAL_1:6;
then
A47: [f.k,f.(k + 1)] in EqR1 \/ EqR2 by A39,A46;
A48: now
per cases by A47,XBOOLE_0:def 3;
suppose
[f.k,f.(k + 1)] in EqR1;
then [f.(k + 1),f.k] in EqR1 by Th6;
hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
end;
suppose
[f.k,f.(k + 1)] in EqR2;
then [f.(k + 1),f.k] in EqR2 by Th6;
hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
end;
end;
1 <= (j + 1) & (j + 1) <= len f by A42,A45,NAT_1:12,13;
then (j + 1) in Seg(len f) by FINSEQ_1:1;
then
A49: g.(j + 1) = f.((len f) + 1 - (1 + j)) by A41
.= f.((len f) - j);
j in Seg(len f) by A42,A44,A45,FINSEQ_1:1;
then g.j = f.(1 + (len f) - j) by A41
.= f.(((len f) - j) + 1);
hence thesis by A49,A48;
end;
len f in Seg(len f) by A36,FINSEQ_1:1;
then g.(len f) = f.(1 + (len f) - len f) by A41
.= f.(1 + 0);
then
A50: x = g.(len g) by A37,A41,FINSEQ_1:def 3;
1 in Seg(len f) by A36,FINSEQ_1:1;
then
A51: g.1 = f.((len f) + 1 - 1) by A41
.= f.(len f);
1 <= len g by A36,A41,FINSEQ_1:def 3;
hence thesis by A2,A34,A38,A51,A50,A43;
end;
Y is_reflexive_in X
proof
let x such that
A52: x in X;
set g = <*x*>;
A53: for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 by
FINSEQ_1:40;
len g = 1 & g.1 = x by FINSEQ_1:40;
hence thesis by A2,A52,A53;
end;
then field Y = X & dom Y = X by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of X by A33,A3,
PARTFUN1:def 2,RELAT_2:def 11,def 16;
for x,y being object holds [x,y] in EqR1 \/ EqR2 implies [x,y] in R1
proof
let x,y be object;
assume
A54: [x,y] in EqR1 \/ EqR2;
set g = <*x,y*>;
A55: len g = 1 + 1 by FINSEQ_1:44;
A57: for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2
proof
let i;
assume that
A58: 1 <= i and
A59: i < len g;
i <= 1 by A55,A59,NAT_1:13;
then 1 = i by A58,XXREAL_0:1;
hence thesis by A54;
end;
len g = 2 by FINSEQ_1:44;
then
A60: g.1 = x & g.(len g) = y;
x in X & y in X by A54,Lm1;
hence thesis by A2,A55,A60,A57;
end;
then EqR1 \/ EqR2 c= R1;
then
A61: EqR1 "\/" EqR2 c= R1 by Def2;
assume [x,y] in EqR1 "\/" EqR2;
then consider f being FinSequence such that
A62: 1 <= len f & x = f.1 &( y = f.(len f) & for i st 1 <= i & i <
len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 ) by A2,A61;
take f;
thus thesis by A62;
end;
given f being FinSequence such that
A63: 1 <= len f and
A64: x = f.1 and
A65: y = f.(len f) and
A66: for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2;
defpred P[Nat] means 1 <= $1 & $1 <= len f implies [f.1,f.$1] in
EqR1 "\/" EqR2;
A67: now
let i;
assume
A68: P[i];
thus P[i+1]
proof
assume that
A69: 1 <= i + 1 and
A70: i + 1 <= len f;
A71: 1 <= i or 1 = i + 1 by A69,NAT_1:8;
A72: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
A73: i < len f by A70,NAT_1:13;
now
per cases by A71;
suppose
A74: 1 <= i;
then [f.i,f.(i+1)] in EqR1 \/ EqR2 by A66,A73;
hence thesis by A68,A70,A72,A74,Th7,NAT_1:13;
end;
suppose
A75: 0 = i;
[f.1,f.1] in EqR1 by A1,A64,Th5;
then [f.1,f.1] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
hence thesis by A72,A75;
end;
end;
hence thesis;
end;
end;
A76: P[0];
for i holds P[i] from NAT_1:sch 2(A76,A67);
hence thesis by A63,A64,A65;
end;
theorem Th29:
for E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x)
proof
let E be Equivalence_Relation of X such that
A1: E = EqR1 \/ EqR2;
for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(
EqR2,x)
proof
let x such that
x in X;
assume that
A2: not Class(E,x) = Class(EqR1,x) and
A3: not Class(E,x) = Class(EqR2,x);
consider y being object such that
A4: y in Class(E,x) & not y in Class(EqR1,x) or y in Class(EqR1,x) &
not y in Class(E,x) by A2,TARSKI:2;
A5: now
assume that
A6: y in Class(EqR1,x) and
A7: not y in Class(E,x);
[y,x] in EqR1 by A6,Th19;
then [y,x] in E by A1,XBOOLE_0:def 3;
hence contradiction by A7,Th19;
end;
then
A8: [y,x] in E by A4,Th19;
consider z being object such that
A9: z in Class(E,x) & not z in Class(EqR2,x) or z in Class(EqR2,x) &
not z in Class(E,x) by A3,TARSKI:2;
A10: now
assume that
A11: z in Class(EqR2,x) and
A12: not z in Class(E,x);
[z,x] in EqR2 by A11,Th19;
then [z,x] in E by A1,XBOOLE_0:def 3;
hence contradiction by A12,Th19;
end;
then
A13: [z,x] in E by A9,Th19;
not [z,x] in EqR2 by A9,A10,Th19;
then
A14: [z,x] in EqR1 by A1,A13,XBOOLE_0:def 3;
A15: now
assume [y,z] in EqR1;
then
A16: [z,y] in EqR1 by Th6;
[x,z] in EqR1 by A14,Th6;
then [x,y] in EqR1 by A16,Th7;
then [y,x] in EqR1 by Th6;
hence contradiction by A4,A5,Th19;
end;
not [y,x] in EqR1 by A4,A5,Th19;
then
A17: [y,x] in EqR2 by A1,A8,XBOOLE_0:def 3;
A18: now
assume
A19: [y,z] in EqR2;
[x,y] in EqR2 by A17,Th6;
then [x,z] in EqR2 by A19,Th7;
then [z,x] in EqR2 by Th6;
hence contradiction by A9,A10,Th19;
end;
[x,z] in E by A13,Th6;
then [y,z] in E by A8,Th7;
hence contradiction by A1,A18,A15,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem
EqR1 \/ EqR2 = nabla X implies EqR1 = nabla X or EqR2 = nabla X
proof
assume
A1: EqR1 \/ EqR2 = nabla X;
X <> {} implies EqR1 = nabla X or EqR2 = nabla X
proof
set y = the Element of X;
A2: now
let x;
assume
A3: x in X;
then
Class(nabla X,x) = Class(EqR1,x) or Class(nabla X,x) = Class(EqR2,x)
by A1,Th29;
hence Class(EqR1,x) = X or Class(EqR2,x) = X by A3,Th26;
end;
assume X <> {};
then Class(EqR1,y) = X or Class(EqR2,y) = X by A2;
hence thesis by Th27;
end;
hence thesis;
end;
definition
let X, EqR;
func Class EqR -> Subset-Family of X means
:Def3:
A in it iff ex x st x in X & A = Class(EqR,x);
existence
proof
defpred P[set] means ex x st x in X & $1 = Class(EqR,x);
consider F being Subset-Family of X such that
A1: for A holds A in F iff P[A] from SUBSET_1:sch 3;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Subset-Family of X;
assume that
A2: for A holds A in F1 iff ex x st x in X & A = Class(EqR,x) and
A3: for A holds A in F2 iff ex x st x in X & A = Class(EqR,x);
now
let A;
A in F1 iff ex x st x in X & A = Class(EqR,x) by A2;
hence A in F1 iff A in F2 by A3;
end;
hence thesis by SETFAM_1:31;
end;
end;
theorem Th31:
X = {} implies Class EqR = {}
proof
assume that
A1: X = {} and
A2: Class EqR <> {};
set z = the Element of Class EqR;
z is Subset of X by A2,TARSKI:def 3;
then ex x st x in X & z = Class(EqR,x) by A2,Def3;
hence contradiction by A1;
end;
definition
let X;
mode a_partition of X -> Subset-Family of X means :Def4:
union it = X &
for A st A in it holds A<>{} & for B st B in it holds A = B or A misses B;
existence
proof
defpred P[set] means ex x st x in X & $1 = {x};
consider F being Subset-Family of X such that
A1: for A being Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;
A2: for A st A in F holds A<>{} & for B st B in F holds A = B or A misses B
proof
let A;
assume A in F;
then consider x such that
x in X and
A3: A = {x} by A1;
thus A <> {} by A3;
let B;
assume B in F;
then consider y such that
y in X and
A4: B = {y} by A1;
now
assume
A5: not x = y;
for z being object st z in A holds not z in B
proof
let z be object;
assume z in A;
then not z = y by A3,A5,TARSKI:def 1;
hence thesis by A4,TARSKI:def 1;
end;
hence A misses B by XBOOLE_0:3;
end;
hence thesis by A3,A4;
end;
take F;
now
let y be object;
now
set Z = {y};
assume
A6: y in X;
then Z is Subset of X by ZFMISC_1:31;
then y in Z & Z in F by A1,A6,TARSKI:def 1;
hence ex Z st y in Z & Z in F;
end;
hence y in X iff ex Z st y in Z & Z in F;
end;
hence thesis by A2,TARSKI:def 4;
end;
end;
theorem Th32:
for P being a_partition of {} holds P = {}
proof
let P be a_partition of {};
assume not thesis;
then consider Z being object such that
A1: Z in P by XBOOLE_0:def 1;
Z <> {} by A1,Def4;
hence thesis by A1;
end;
registration let X be empty set;
cluster -> empty for a_partition of X;
coherence by Th32;
end;
registration let X be empty set;
cluster empty for a_partition of X;
existence
proof
take the a_partition of X;
thus thesis;
end;
end;
::$L https://en.wikipedia.org/wiki/Equivalence_relation#Fundamental_theorem_of_equivalence_relations Equivalence relation
theorem Th33:
Class EqR is a_partition of X
proof
now
let x be object;
now
consider Z such that
A1: Z = Class(EqR,x);
assume
A2: x in X;
then Z in Class EqR by A1,Def3;
hence ex Z st x in Z & Z in Class EqR by A2,A1,Th20;
end;
hence x in X iff ex Z st x in Z & Z in Class EqR;
end;
hence union(Class EqR) = X by TARSKI:def 4;
let A;
assume A in Class EqR;
then
A3: ex x st x in X & A = Class(EqR,x) by Def3;
hence A <> {} by Th20;
let B;
assume B in Class EqR;
then ex y st y in X & B = Class(EqR,y) by Def3;
hence thesis by A3,Th24;
end;
::$L https://en.wikipedia.org/wiki/Equivalence_relation#Fundamental_theorem_of_equivalence_relations Equivalence relation
theorem Th34:
for P being a_partition of X holds ex EqR st P = Class EqR
proof
let P be a_partition of X;
A1: X <> {} implies ex EqR st P = Class EqR
proof
defpred P[object,object] means ex A st A in P & $1 in A & $2 in A;
assume X <> {};
A2: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof
let x,y,z;
given A such that
A3: A in P and
A4: x in A & y in A;
given B such that
A5: B in P and
A6: y in B & z in B;
A = B or A misses B by A3,A5,Def4;
hence thesis by A3,A4,A6,XBOOLE_0:3;
end;
A7: union P = X by Def4;
A8: for x st x in X holds P[x,x]
proof
let x;
assume x in X;
then consider Z such that
A9: x in Z and
A10: Z in P by A7,TARSKI:def 4;
reconsider A = Z as Subset of X by A10;
take A;
thus thesis by A9,A10;
end;
A11: for x,y st P[x,y] holds P[y,x];
consider R being Equivalence_Relation of X such that
A12: for x,y holds [x,y] in R iff x in X & y in X & P[x,y] from
ExEqRel(A8,A11,A2);
take R;
now
let A;
A13: now
set x = the Element of A;
assume
A14: A in P;
then
A15: A <> {} by Def4;
then
A16: x in X by TARSKI:def 3;
now
let y be object;
A17: now
assume y in Class(R,x);
then [y,x] in R by Th19;
then consider B such that
A18: B in P & y in B and
A19: x in B by A12;
A meets B by A15,A19,XBOOLE_0:3;
hence y in A by A14,A18,Def4;
end;
now
assume y in A;
then [y,x] in R by A12,A14,A16;
hence y in Class(R,x) by Th19;
end;
hence y in A iff y in Class(R,x) by A17;
end;
then A = Class(R,x) by TARSKI:2;
hence A in Class R by A16,Def3;
end;
now
assume A in Class R;
then consider x such that
A20: x in X and
A21: A = Class(R,x) by Def3;
x in Class(R,x) by A20,Th20;
then [x,x] in R by Th19;
then consider B such that
A22: B in P and
A23: x in B and
x in B by A12;
now
let y be object;
A24: now
assume y in A;
then [y,x] in R by A21,Th19;
then consider C such that
A25: C in P & y in C and
A26: x in C by A12;
B meets C by A23,A26,XBOOLE_0:3;
hence y in B by A22,A25,Def4;
end;
now
assume y in B;
then [y,x] in R by A12,A22,A23;
hence y in A by A21,Th19;
end;
hence y in A iff y in B by A24;
end;
hence A in P by A22,TARSKI:2;
end;
hence A in P iff A in Class R by A13;
end;
hence thesis by SETFAM_1:31;
end;
X = {} implies ex EqR st P = Class EqR
proof
set EqR1 = the Equivalence_Relation of X;
assume
A27: X = {};
take EqR1;
P = {} by A27;
hence thesis by A27,Th31;
end;
hence thesis by A1;
end;
theorem
for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y) by Lm2;
theorem
x in Class EqR implies ex y being Element of X st x = Class(EqR,y)
proof
assume
A1: x in Class EqR;
then reconsider x as Subset of X;
consider y such that
A2: y in X and
A3: x = Class(EqR,y) by A1,Def3;
reconsider y as Element of X by A2;
take y;
thus thesis by A3;
end;
begin :: Addenda
:: from FSM_1, PARTIT1, 2005.02.06, A.T.
registration
let X be non empty set;
cluster -> non empty for a_partition of X;
coherence
proof
set x = the Element of X;
let P be a_partition of X;
union P = X by Def4;
then ex A being set st x in A & A in P by TARSKI:def 4;
hence thesis;
end;
end;
:: from PUA2MSS1
registration
let X be set;
cluster -> with_non-empty_elements for a_partition of X;
coherence
proof
let P be a_partition of X;
assume {} in P;
hence contradiction by Def4;
end;
end;
definition
let X be set, R be Equivalence_Relation of X;
redefine func Class R -> a_partition of X; :: redefines Class (EQREL_1, definition)
coherence by Th33;
end;
:: from PRALG_3
registration
let I be non empty set, R be Equivalence_Relation of I;
cluster Class R -> non empty;
coherence;
end;
registration
let I be non empty set, R be Equivalence_Relation of I;
cluster Class R -> with_non-empty_elements;
coherence;
end;
notation
let I be non empty set, R be Equivalence_Relation of I;
let x be Element of I;
synonym EqClass↑(R,x) for Class(R,x);
end;
definition
let I be non empty set, R be Equivalence_Relation of I;
let x be Element of I;
redefine func EqClass(R,x) -> Element of Class R; :: redefines EqClass (EQREL_1, synonym) → Class (EQREL_1, synonym) → Im (RELAT_1, definition)
coherence
proof
thus Class(R,x) is Element of Class R by Def3;
end;
end;
definition
let X be set;
func SmallestPartition X -> set equals
Class id X;
coherence;
end;
definition
let X be set;
redefine func SmallestPartition X -> a_partition of X; :: redefines SmallestPartition (EQREL_1, definition)
correctness;
end;
theorem
for X being non empty set holds
SmallestPartition X = the set of all {x} where x is Element of X
proof
let X be non empty set;
set Y = the set of all {x} where x is Element of X;
hereby
let x be object;
assume x in SmallestPartition X;
then consider y being object such that
A1: y in X and
A2: x = Class(id X, y) by Def3;
x = {y} by A1,A2,Th25;
hence x in Y by A1;
end;
let x be object;
assume x in Y;
then consider y being Element of X such that
A3: x = {y};
Class(id X, y) = x by A3,Th25;
hence thesis by Def3;
end;
:: from T_1TOPSP, 30.12.2006, AK
:: Classes of partitions of a set
reserve X for non empty set,
x for Element of X;
definition
let X be non empty set,x be Element of X,S1 be a_partition of X;
func EqClass(x,S1) -> Subset of X means
:Def6:
x in it & it in S1;
existence
proof
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
take Class(EQR,x);
thus x in Class(EQR,x) by Th20;
thus thesis by A1,Def3;
end;
uniqueness by Def4,XBOOLE_0:3;
end;
theorem Th38:
for S1,S2 being a_partition of X st (for x being Element of X
holds EqClass(x,S1) = EqClass(x,S2)) holds S1=S2
proof
let S1,S2 be a_partition of X;
assume
A1: for x being Element of X holds EqClass(x,S1) = EqClass(x,S2);
now
let P be Subset of X;
thus P in S1 implies P in S2
proof
set x = the Element of P;
assume
A2: P in S1;
then
A3: P is non empty by Def4;
then x in P;
then reconsider x as Element of X;
P = EqClass(x,S1) by A2,A3,Def6;
then P = EqClass(x,S2) by A1;
hence thesis by Def6;
end;
thus P in S2 implies P in S1
proof
set x = the Element of P;
assume
A4: P in S2;
then
A5: P <> {} by Def4;
then x in P;
then reconsider x as Element of X;
P = EqClass(x,S2) by A4,A5,Def6;
then P = EqClass(x,S1) by A1;
hence thesis by Def6;
end;
end;
hence thesis by SETFAM_1:31;
end;
theorem Th39:
for X being non empty set holds {X} is a_partition of X
proof
let X be non empty set;
reconsider A1 = {X} as Subset-Family of X by ZFMISC_1:68;
A1: for A being Subset of X st A in A1 holds A <> {} & for B being Subset of
X st B in A1 holds A = B or A misses B
proof
let A be Subset of X;
assume
A2: A in A1;
hence A <> {} by TARSKI:def 1;
let B be Subset of X;
assume B in A1;
then B = X by TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
union A1 = X;
hence thesis by A1,Def4;
end;
definition
let X be set;
mode Family-Class of X is Subset-Family of bool X;
end;
definition
let X be set;
let F be Family-Class of X;
attr F is partition-membered means :Def7:
for S being set st S in F holds S is a_partition of X;
end;
registration
let X be set;
cluster partition-membered for Family-Class of X;
existence
proof
reconsider E = {} as Family-Class of X by XBOOLE_1:2;
take E;
let S be set;
assume S in E;
hence thesis;
end;
end;
definition
let X be set;
mode Part-Family of X is partition-membered Family-Class of X;
end;
reserve F for Part-Family of X;
registration
let X be non empty set;
cluster non empty for a_partition of X;
existence
proof
take {X};
thus thesis by Th39;
end;
end;
theorem Th40:
for X being set, p being a_partition of X holds {p} is Part-Family of X
proof
let X be set;
let p be a_partition of X;
for x be set st x in {p} holds x is a_partition of X by TARSKI:def 1;
hence thesis by Def7;
end;
registration
let X be set;
cluster non empty for Part-Family of X;
existence
proof
set p = the a_partition of X;
reconsider P = {p} as Part-Family of X by Th40;
take P;
thus thesis;
end;
end;
theorem Th41:
for S1 being a_partition of X, x,y being Element of X holds
EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1)
proof
let S1 be a_partition of X;
let x,y be Element of X;
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
A2: y in Class(EQR,y) by Th20;
Class(EQR,y) in S1 by A1,Def3;
then
A3: Class(EQR,y) = EqClass(y,S1) by A2,Def6;
A4: x in Class(EQR,x) by Th20;
Class(EQR,x) in S1 by A1,Def3;
then
A5: Class(EQR,x) = EqClass(x,S1) by A4,Def6;
assume EqClass(x,S1) meets EqClass(y,S1);
hence thesis by A5,A3,Th24;
end;
Lm3: for A being set holds A in {EqClass(x,S) where S is a_partition of X : S
in F} implies ex T being a_partition of X st T in F & A = EqClass(x,T)
proof
let A be set;
assume A in {EqClass(x,S) where S is a_partition of X : S in F};
then consider S being a_partition of X such that
A1: A = EqClass(x,S) & S in F;
take S;
thus thesis by A1;
end;
theorem
for A being set,X being non empty set,S being a_partition of X holds A
in S implies ex x being Element of X st A = EqClass(x,S)
proof
let A be set,X be non empty set,S be a_partition of X;
assume
A1: A in S;
then A is non empty by Def4;
then consider x being object such that
A2: x in A;
take x;
thus thesis by A1,A2,Def6;
end;
definition
let X be non empty set,F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means
for x being Element
of X holds EqClass(x,it) = meet{EqClass(x,S) where S is a_partition of X : S in
F};
uniqueness
proof
given S1,S2 being a_partition of X such that
A1: for x being Element of X holds EqClass(x,S1) = meet{EqClass(x,S)
where S is a_partition of X : S in F} and
A2: for x being Element of X holds EqClass(x,S2) = meet{EqClass(x,S)
where S is a_partition of X : S in F} and
A3: not S1 = S2;
now
let x be Element of X;
EqClass(x,S1) = meet{EqClass(x,S) where S is a_partition of X : S in
F} by A1;
hence EqClass(x,S1) = EqClass(x,S2) by A2;
end;
hence contradiction by A3,Th38;
end;
existence
proof
thus ex G being non empty a_partition of X st for x being Element of X
holds EqClass(x,G) = meet{EqClass(x,S) where S is a_partition of X : S in F}
proof
set G = the set of all
meet{EqClass(x,S) where S is a_partition of X : S in F} where x
is Element of X;
G c= bool X
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in G;
then consider x being Element of X such that
A4: y = meet{EqClass(x,S) where S is a_partition of X : S in F};
yy c= X
proof
let e be object;
consider T being object such that
A5: T in F by XBOOLE_0:def 1;
reconsider T as a_partition of X by A5,Def7;
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
in F } by A5;
then consider f being set such that
A6: f in {EqClass(x,S) where S is a_partition of X : S in F};
consider S being a_partition of X such that
A7: f = EqClass(x,S) and
S in F by A6;
assume e in yy;
then e in EqClass(x,S) by A4,A6,A7,SETFAM_1:def 1;
hence thesis;
end;
hence thesis;
end;
then reconsider G as Subset-Family of X;
G is a_partition of X
proof
X c= union G
proof
let a be object;
consider T being object such that
A8: T in F by XBOOLE_0:def 1;
assume a in X;
then reconsider a1=a as Element of X;
reconsider T as a_partition of X by A8,Def7;
A9: meet{EqClass(a1,S) where S is a_partition of X : S in F} in G;
A10: for T being set st T in {EqClass(a1,S) where S is a_partition
of X : S in F} holds a1 in T
proof
let T be set;
assume T in {EqClass(a1,S) where S is a_partition of X : S in F};
then ex A being a_partition of X st T = EqClass(a1,A) & A in F;
hence thesis by Def6;
end;
EqClass(a1,T) in {EqClass(a1,S) where S is a_partition of X : S
in F} by A8;
then
a in meet{EqClass(a1,S) where S is a_partition of X: S in F} by A10,
SETFAM_1:def 1;
hence thesis by A9,TARSKI:def 4;
end;
hence union G = X;
let A be Subset of X;
consider T being object such that
A11: T in F by XBOOLE_0:def 1;
reconsider T as a_partition of X by A11,Def7;
assume
A12: A in G;
then consider x being Element of X such that
A13: A = meet{EqClass(x,S) where S is a_partition of X : S in F};
A14: for Y being set st Y in {EqClass(x,S) where S is a_partition of X
: S in F} holds x in Y
proof
let Y be set;
assume Y in {EqClass(x,S) where S is a_partition of X : S in F};
then ex T being a_partition of X st Y = EqClass(x,T) & T in F;
hence thesis by Def6;
end;
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S in
F} by A11;
hence A<>{} by A13,A14,SETFAM_1:def 1;
consider x being Element of X such that
A15: A = meet{EqClass(x,S) where S is a_partition of X : S in F} by A12;
let B be Subset of X;
assume B in G;
then consider y being Element of X such that
A16: B = meet{EqClass(y,S) where S is a_partition of X : S in F};
thus A = B or A misses B
proof
A17: {EqClass(y,S) where S is a_partition of X : S in F} is non empty
proof
consider T being object such that
A18: T in F by XBOOLE_0:def 1;
reconsider T as a_partition of X by A18,Def7;
EqClass(y,T) in {EqClass(y,S) where S is a_partition of X : S
in F} by A18;
hence thesis;
end;
A19: {EqClass(x,S) where S is a_partition of X : S in F} is non empty
proof
consider T being object such that
A20: T in F by XBOOLE_0:def 1;
reconsider T as a_partition of X by A20,Def7;
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
in F} by A20;
hence thesis;
end;
now
assume A meets B;
then consider c being object such that
A21: c in A & c in B by XBOOLE_0:3;
c in meet{EqClass(x,S) where S is a_partition of X : S in F}
/\ meet{EqClass(y,S) where S is a_partition of X : S in F} by A15,A16,A21,
XBOOLE_0:def 4;
then
A22: c in meet({EqClass(x,S) where S is a_partition of X: S in F }
\/ {EqClass(y,S) where S is a_partition of X : S in F}) by A19,A17,SETFAM_1:9;
A23: now
let T be a_partition of X;
assume T in F;
then
EqClass(y,T) in {EqClass(y,S) where S is a_partition of X :
S in F};
then
EqClass(y,T) in {EqClass(x,S) where S is a_partition of X :
S in F} \/ {EqClass(y,S) where S is a_partition of X : S in F} by
XBOOLE_0:def 3;
hence c in EqClass(y,T) by A22,SETFAM_1:def 1;
end;
A24: now
let T be a_partition of X;
assume T in F;
then
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X :
S in F};
then
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X :
S in F} \/ {EqClass(y,S) where S is a_partition of X : S in F} by
XBOOLE_0:def 3;
hence c in EqClass(x,T) by A22,SETFAM_1:def 1;
end;
A25: for T being a_partition of X st T in F
ex A being object
st A in EqClass(x,T) & A in EqClass(y,T)
proof
let T be a_partition of X;
assume
A26: T in F;
take c;
thus thesis by A24,A23,A26;
end;
A27: for T being a_partition of X st T in F holds (EqClass(x,T))
meets (EqClass(y,T))
proof
let T be a_partition of X;
assume T in F;
then ex A being object
st A in EqClass(x,T) & A in EqClass(y,T) by
A25;
hence thesis by XBOOLE_0:3;
end;
A28: {EqClass(y,S) where S is a_partition of X : S in F} c= {
EqClass(x,S) where S is a_partition of X : S in F}
proof
let A be object;
assume A in {EqClass(y,S) where S is a_partition of X : S in F };
then consider T being a_partition of X such that
A29: T in F and
A30: A = EqClass(y,T) by Lm3;
A = EqClass(x,T) by A27,A29,A30,Th41;
hence thesis by A29;
end;
{EqClass(x,S) where S is a_partition of X : S in F} c= {
EqClass(y,S) where S is a_partition of X : S in F}
proof
let A be object;
assume A in {EqClass(x,S) where S is a_partition of X : S in F };
then consider T being a_partition of X such that
A31: T in F and
A32: A = EqClass(x,T) by Lm3;
A = EqClass(y,T) by A27,A31,A32,Th41;
hence thesis by A31;
end;
hence thesis by A15,A16,A28,XBOOLE_0:def 10;
end;
hence thesis;
end;
end;
then reconsider G as non empty a_partition of X;
take G;
for x being Element of X holds EqClass(x,G) = meet{EqClass(x,S)
where S is a_partition of X : S in F}
proof
let x be Element of X;
A33: now
let Y be set;
assume Y in {EqClass(x,S) where S is a_partition of X : S in F};
then ex T being a_partition of X st Y = EqClass(x,T) & T in F;
hence x in Y by Def6;
end;
{EqClass(x,S) where S is a_partition of X : S in F} is non empty
proof
consider T being object such that
A34: T in F by XBOOLE_0:def 1;
reconsider T as a_partition of X by A34,Def7;
EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
in F} by A34;
hence thesis;
end;
then meet{EqClass(x,S) where S is a_partition of X : S in F} in G & x
in meet{ EqClass(x,S) where S is a_partition of X : S in F} by A33,
SETFAM_1:def 1;
hence thesis by Def6;
end;
hence thesis;
end;
end;
end;
theorem Th43:
for X being non empty set, S being a_partition of X,
A being Subset of S holds (union S) \ (union A) = union (S \ A)
proof
let X be non empty set;
let S be a_partition of X;
let A be Subset of S;
thus (union S) \ (union A) c= union (S \ A)
proof
let y be object;
assume
A1: y in (union S) \ (union A);
then y in (union S) by XBOOLE_0:def 5;
then consider z being set such that
A2: y in z and
A3: z in S by TARSKI:def 4;
not y in (union A) by A1,XBOOLE_0:def 5;
then not z in A by A2,TARSKI:def 4;
then z in S \ A by A3,XBOOLE_0:def 5;
hence thesis by A2,TARSKI:def 4;
end;
thus union (S \ A) c= (union S) \ (union A)
proof
let y be object;
assume y in union(S \ A);
then consider z being set such that
A4: y in z and
A5: z in S \ A by TARSKI:def 4;
A6: z in S by A5,XBOOLE_0:def 5;
A7: not z in A by A5,XBOOLE_0:def 5;
A8: now
let w be set;
assume
A9: w in A;
then w in S;
then z misses w by A6,A7,A9,Def4;
hence not y in w by A4,XBOOLE_0:3;
end;
A10: now
assume y in union A;
then ex v being set st y in v & v in A by TARSKI:def 4;
hence contradiction by A8;
end;
y in union S by A4,A6,TARSKI:def 4;
hence thesis by A10,XBOOLE_0:def 5;
end;
end;
theorem
for X being non empty set,A being Subset of X, S being a_partition of
X holds A in S implies union(S \ {A}) = X \ A
proof
let X be non empty set;
let A be Subset of X;
let S be a_partition of X;
assume
A1: A in S;
{A} c= S by A1,TARSKI:def 1;
then reconsider AA = {A} as Subset of S;
thus union (S \ {A}) = (union S) \ (union AA) by Th43
.= X \ (union {A}) by Def4
.= X \ A;
end;
:: Added 2007.10.17, AK
registration
let A be empty set;
cluster -> empty for a_partition of A;
coherence;
end;
theorem
{} is a_partition of {}
proof
reconsider A = {} as Subset-Family of {} by XBOOLE_1:2;
union A = {} & for a be Subset of {} st a in A holds a<>{} & for b be
Subset of {} st b in A holds a = b or a misses b;
hence thesis by Def4;
end;
registration
let A be empty set;
cluster empty for a_partition of A;
existence
proof
take the a_partition of A;
thus thesis;
end;
end;
begin :: Moved from BORSUK_1, 2010.03.15, A.T.
reserve e,u,v for object, E,X,Y,X1 for set;
theorem
for F being Function st X c= F"X1 holds F.:X c= X1
proof
let F be Function;
assume X c= F"X1;
then
A1: F.:X c= F.:F"X1 by RELAT_1:123;
F.:F"X1 c= X1 by FUNCT_1:75;
hence thesis by A1;
end;
theorem Th47:
E c= [:X,Y:] implies (.:pr1(X,Y)).E = pr1(X,Y).:E
proof
assume E c= [:X,Y:];
then E c= dom pr1(X,Y) by FUNCT_3:def 4;
hence thesis by FUNCT_3:def 1;
end;
theorem Th48:
E c= [:X,Y:] implies (.:pr2(X,Y)).E = pr2(X,Y).:E
proof
assume E c= [:X,Y:];
then E c= dom pr2(X,Y) by FUNCT_3:def 5;
hence thesis by FUNCT_3:def 1;
end;
theorem Th49:
for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
{} holds pr1(X,Y).:[:X1,Y1:] = X1 & pr2(X,Y).:[:X1,Y1:] = Y1
proof
let X1 be Subset of X, Y1 be Subset of Y;
assume
A1: [:X1,Y1:] <> {};
then
A2: X1 <> {};
A3: Y1 <> {} by A1;
A4: X <> {} by A2;
now
set y = the Element of Y1;
let x be object;
thus x in pr1(X,Y).:[:X1,Y1:] implies x in X1
proof
assume x in pr1(X,Y).:[:X1,Y1:];
then consider u such that
A5: u in [:X,Y:] and
A6: u in [:X1,Y1:] & x = pr1(X,Y).u by FUNCT_2:64;
A7: u`2 in Y by A5,MCART_1:10;
u`1 in X1 & x = pr1(X,Y).(u`1,u`2) by A6,MCART_1:10,21;
hence thesis by A7,FUNCT_3:def 4;
end;
assume
A8: x in X1;
y in Y by A3,TARSKI:def 3;
then
A9: x = pr1(X,Y).(x,y) by A8,FUNCT_3:def 4;
[x,y] in [:X1,Y1:] by A3,A8,ZFMISC_1:87;
hence x in pr1(X,Y).:[:X1,Y1:] by A4,A9,FUNCT_2:35;
end;
hence pr1(X,Y).:[:X1,Y1:] = X1 by TARSKI:2;
A10: Y <> {} by A3;
now
set x = the Element of X1;
let y be object;
thus y in pr2(X,Y).:[:X1,Y1:] implies y in Y1
proof
assume y in pr2(X,Y).:[:X1,Y1:];
then consider u such that
A11: u in [:X,Y:] and
A12: u in [:X1,Y1:] & y = pr2(X,Y).u by FUNCT_2:64;
A13: u`1 in X by A11,MCART_1:10;
u`2 in Y1 & y = pr2(X,Y).(u`1,u`2) by A12,MCART_1:10,21;
hence thesis by A13,FUNCT_3:def 5;
end;
assume
A14: y in Y1;
x in X by A2,TARSKI:def 3;
then
A15: y = pr2(X,Y).(x,y) by A14,FUNCT_3:def 5;
[x,y] in [:X1,Y1:] by A2,A14,ZFMISC_1:87;
hence y in pr2(X,Y).:[:X1,Y1:] by A10,A15,FUNCT_2:35;
end;
hence thesis by TARSKI:2;
end;
theorem Th50:
for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
{} holds .:pr1(X,Y). [:X1,Y1:] = X1 & .:pr2(X,Y). [:X1,Y1:] = Y1
proof
let X1 be Subset of X, Y1 be Subset of Y;
assume
A1: [:X1,Y1:] <> {};
thus .:pr1(X,Y). [:X1,Y1:] = pr1(X,Y).:[:X1,Y1:] by Th47
.= X1 by A1,Th49;
thus .:pr2(X,Y). [:X1,Y1:] = pr2(X,Y).:[:X1,Y1:] by Th48
.= Y1 by A1,Th49;
end;
theorem
for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:]
st for E st E in H holds E c= A &
ex X1 being Subset of X, Y1 being Subset of Y
st E =[:X1,Y1:] holds [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):] c= A
proof
let A be Subset of [:X,Y:], H be Subset-Family of [:X,Y:] such that
A1: for E st E in H holds E c= A & ex X1 being Subset of X, Y1 being
Subset of Y st E =[:X1,Y1:];
let u,v be object;
assume
A2: [u,v] in [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):];
then
A3: v in meet(.:pr2(X,Y).:H) by ZFMISC_1:87;
u in union(.:pr1(X,Y).:H) by A2,ZFMISC_1:87;
then consider x being set such that
A4: u in x and
A5: x in .:pr1(X,Y).:H by TARSKI:def 4;
consider y being object such that
y in dom .:pr1(X,Y) and
A6: y in H and
A7: x = .:pr1(X,Y).y by A5,FUNCT_1:def 6;
reconsider y as set by TARSKI:1;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y =[:X1,Y1:] by A1,A6;
A9: y <> {} by A4,A7,FUNCT_3:8;
y in bool[:X,Y:] by A6;
then y in bool dom pr2(X,Y) by FUNCT_3:def 5;
then y in dom .:pr2(X,Y) by FUNCT_3:def 1;
then .:pr2(X,Y).y in .:pr2(X,Y).:H by A6,FUNCT_1:def 6;
then Y1 in .:pr2(X,Y).:H by A8,A9,Th50;
then
A10: v in Y1 by A3,SETFAM_1:def 1;
u in X1 by A4,A7,A8,A9,Th50;
then
A11: [u,v] in y by A8,A10,ZFMISC_1:87;
y c= A by A1,A6;
hence thesis by A11;
end;
theorem
for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for E
st E in H holds E c= A & ex X1 being Subset of X, Y1 being Subset of Y
st E = [:X1,Y1:]
holds [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):] c= A
proof
let A be Subset of [:X,Y:], H be Subset-Family of [:X,Y:] such that
A1: for E st E in H holds E c= A & ex X1 being Subset of X, Y1 being
Subset of Y st E =[:X1,Y1:];
let u,v be object;
assume
A2: [u,v] in [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):];
then
A3: u in meet(.:pr1(X,Y).:H) by ZFMISC_1:87;
v in union(.:pr2(X,Y).:H) by A2,ZFMISC_1:87;
then consider x being set such that
A4: v in x and
A5: x in .:pr2(X,Y).:H by TARSKI:def 4;
consider y being object such that
y in dom .:pr2(X,Y) and
A6: y in H and
A7: x = .:pr2(X,Y).y by A5,FUNCT_1:def 6;
reconsider y as set by TARSKI:1;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y =[:X1,Y1:] by A1,A6;
A9: y <> {} by A4,A7,FUNCT_3:8;
y in bool[:X,Y:] by A6;
then y in bool dom pr1(X,Y) by FUNCT_3:def 4;
then y in dom .:pr1(X,Y) by FUNCT_3:def 1;
then .:pr1(X,Y).y in .:pr1(X,Y).:H by A6,FUNCT_1:def 6;
then X1 in .:pr1(X,Y).:H by A8,A9,Th50;
then
A10: u in X1 by A3,SETFAM_1:def 1;
v in Y1 by A4,A7,A8,A9,Th50;
then
A11: [u,v] in y by A8,A10,ZFMISC_1:87;
y c= A by A1,A6;
hence thesis by A11;
end;
theorem
for X being set, Y being non empty set, f being Function of X,Y
for H being Subset-Family of X holds union(.:f.:H) = f.: union H
proof
let X be set, Y be non empty set, f be Function of X,Y;
let H be Subset-Family of X;
dom f = X by FUNCT_2:def 1;
hence thesis by FUNCT_3:14;
end;
reserve X,Y,Z for non empty set;
theorem
for X being set, a being Subset-Family of X holds union union a
= union { union A where A is Subset of X: A in a }
proof
let X be set, a be Subset-Family of X;
thus union union a c= union { union A where A is Subset of X: A in a }
proof
let e be object;
assume e in union union a;
then consider B being set such that
A1: e in B and
A2: B in union a by TARSKI:def 4;
consider C being set such that
A3: B in C and
A4: C in a by A2,TARSKI:def 4;
A5: union C in { union A where A is Subset of X: A in a } by A4;
e in union C by A1,A3,TARSKI:def 4;
hence thesis by A5,TARSKI:def 4;
end;
let e be object;
assume e in union { union A where A is Subset of X: A in a };
then consider c being set such that
A6: e in c and
A7: c in { union A where A is Subset of X: A in a } by TARSKI:def 4;
consider A being Subset of X such that
A8: c = union A and
A9: A in a by A7;
consider b being set such that
A10: e in b and
A11: b in A by A6,A8,TARSKI:def 4;
b in union a by A9,A11,TARSKI:def 4;
hence thesis by A10,TARSKI:def 4;
end;
theorem Th55:
for X being set for D being Subset-Family of X st union D = X
for A being Subset of D, B being Subset of X st B = union A holds
B` c= union A`
proof
let X be set;
let D be Subset-Family of X such that
A1: union D = X;
let A be Subset of D, B be Subset of X such that
A2: B = union A;
let e be object;
assume
A3: e in B`;
then consider u being set such that
A4: e in u and
A5: u in D by A1,TARSKI:def 4;
not e in B by A3,XBOOLE_0:def 5;
then not u in A by A2,A4,TARSKI:def 4;
then u in A` by A5,SUBSET_1:29;
hence thesis by A4,TARSKI:def 4;
end;
theorem
for F being Function of X,Y, G being Function of X,Z st
for x,x9 being Element of X st F.x=F.x9 holds G.x=G.x9
ex H being Function of Y,Z st H*F = G
proof
let F be Function of X,Y, G be Function of X,Z;
defpred P[object,object] means
not (ex x being Element of X st $1 = F.x) or for x
being Element of X st $1 = F.x holds $2 = G.x;
assume
A1: for x,x9 being Element of X st F.x=F.x9 holds G.x=G.x9;
A2: now
let e be object such that
e in Y;
now
per cases;
case
ex x being Element of X st e = F.x;
then consider x being Element of X such that
A3: e = F.x;
take u = G.x;
thus u in Z & ((ex x being Element of X st e = F.x) implies ex x being
Element of X st e = F.x & u = G.x) by A3;
end;
case
A4: not ex x being Element of X st e = F.x;
set u = the Element of Z;
u in Z;
hence
ex u st u in Z & ((ex x being Element of X st e = F.x) implies ex
x being Element of X st e = F.x & u = G.x) by A4;
end;
end;
then consider u such that
A5: u in Z and
A6: (ex x being Element of X st e = F.x) implies ex x being Element of
X st e = F.x & u = G.x;
reconsider u as object;
take u;
thus u in Z by A5;
thus P[e,u] by A1,A6;
end;
consider H being Function of Y,Z such that
A7: for e being object st e in Y holds P[e,H.e] from FUNCT_2:sch 1(A2);
take H;
now
let x be Element of X;
thus (H*F).x = H.(F.x) by FUNCT_2:15
.= G.x by A7;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for X,Y,Z for y being Element of Y, F being (Function of X,Y),
G being Function of Y,Z holds F"{y} c= (G*F)"{G.y}
proof
let X,Y,Z;
let y be Element of Y, F be (Function of X,Y), G be Function of Y,Z;
F"{y} c= (G*F)"Im(G,y) by FUNCT_2:44;
hence thesis by SETWISEO:8;
end;
theorem
for F being Function of X,Y, x being Element of X,
z being Element of Z holds [:F,id Z:].(x,z) = [F.x,z]
proof
let F be Function of X,Y, x be Element of X, z be Element of Z;
thus [:F,id Z:].(x,z) = [F.x, (id Z).z] by FUNCT_3:75
.= [F.x,z];
end;
theorem
for F being Function of X,Y, A being Subset of X, B being Subset of Z
holds [:F,id Z:].:[:A,B:] = [:F.:A,B:]
proof
let F be Function of X,Y, A be Subset of X, B be Subset of Z;
thus [:F,id Z:].:[:A,B:] = [:F.:A, (id Z).:B:] by FUNCT_3:72
.= [:F.:A,B:] by FUNCT_1:92;
end;
theorem
for F being Function of X,Y, y being Element of Y,
z being Element of Z holds [:F,id Z:]"{[y,z]} = [:F"{y},{z}:]
proof
let F be Function of X,Y, y be Element of Y, z be Element of Z;
thus [:F,id Z:]"{[y,z]} = [:F,id Z:]"[:{y},{z}:] by ZFMISC_1:29
.= [:F"{y},(id Z)"{z}:] by FUNCT_3:73
.= [:F"{y},{z}:] by FUNCT_2:94;
end;
theorem
for D being Subset-Family of X, A being Subset of D holds
union A is Subset of X
proof
let D be Subset-Family of X, A be Subset of D;
union A c= X
proof
let e be object;
assume e in union A;
then ex u being set st e in u & u in A by TARSKI:def 4;
then e in union D by TARSKI:def 4;
hence thesis;
end;
hence thesis;
end;
theorem
for X being set, D being a_partition of X, A,B being Subset of D
holds union(A /\ B) = union A /\ union B
proof
let X be set, D be a_partition of X, A,B be Subset of D;
thus union(A/\B) c= union A /\ union B by ZFMISC_1:79;
let e be object;
assume
A1: e in union A /\ union B;
then e in union A by XBOOLE_0:def 4;
then consider a being set such that
A2: e in a and
A3: a in A by TARSKI:def 4;
A4: a in D by A3;
e in union B by A1,XBOOLE_0:def 4;
then consider b being set such that
A5: e in b and
A6: b in B by TARSKI:def 4;
A7: b in D by A6;
not a misses b by A2,A5,XBOOLE_0:3;
then a = b by A4,A7,Def4;
then a in A/\B by A3,A6,XBOOLE_0:def 4;
hence thesis by A2,TARSKI:def 4;
end;
theorem
for D being a_partition of X, A being Subset of D, B being
Subset of X st B = union A holds B` = union A`
proof
let D be a_partition of X, A be Subset of D, B be Subset of X;
assume
A1: B = union A;
union D = X by Def4;
hence B` c= union A` by A1,Th55;
let e be object;
assume e in union A`;
then consider u being set such that
A2: e in u and
A3: u in A` by TARSKI:def 4;
A4: u in D by A3;
assume not e in B`;
then e in B by A2,A4,SUBSET_1:29;
then consider v being set such that
A5: e in v and
A6: v in A by A1,TARSKI:def 4;
A7: v in D by A6;
not u misses v by A2,A5,XBOOLE_0:3;
then u = v by A4,A7,Def4;
hence contradiction by A3,A6,XBOOLE_0:def 5;
end;
theorem :: Class(id X) is non-empty
for E being Equivalence_Relation of X holds Class(E) is non empty;
definition
let X;
let D be non empty a_partition of X;
func proj D -> Function of X, D means
:Def9:
for p being Element of X holds p in it.p;
existence
proof
defpred P[object,object] means ex A being set st A = $2 & $1 in A;
A1: now
A2: union D = X by Def4;
let e be object;
assume e in X;
then ex u being set st e in u & u in D by A2,TARSKI:def 4;
hence ex u being object st u in D & P[e,u];
end;
consider F being Function of X, D such that
A3: for e being object st e in X holds P[e,F.e] from FUNCT_2:sch 1(A1);
take F;
let p be Element of X;
P[p,F.p] by A3;
hence thesis;
end;
correctness
proof
let F,G be Function of X,D such that
A4: ( for p being Element of X holds p in F.p)& for p being Element of
X holds p in G.p;
now
let x be Element of X;
x in F.x & x in G.x by A4;
then
A5: not F.x misses G.x by XBOOLE_0:3;
F.x is Subset of X & G.x is Subset of X by TARSKI:def 3;
hence F.x = G.x by A5,Def4;
end;
hence F = G by FUNCT_2:63;
end;
end;
theorem Th65:
for D being non empty a_partition of X, p being Element of X,
A being Element of D st p in A holds A = (proj D).p
proof
let D be non empty a_partition of X, p be Element of X, A be Element of D
such that
A1: p in A;
p in (proj D).p by Def9;
then (proj D).p is Subset of X & not (proj D).p misses A by A1,TARSKI:def 3
,XBOOLE_0:3;
hence thesis by Def4;
end;
theorem
for D being non empty a_partition of X, p being Element of D
holds p = proj D " {p}
proof
let D be non empty a_partition of X, p be Element of D;
thus p c= proj D " {p}
proof
let e be object;
assume
A1: e in p;
then (proj D).e = p by Th65;
then (proj D).e in {p} by TARSKI:def 1;
hence thesis by A1,FUNCT_2:38;
end;
let e be object;
assume
A2: e in proj D " {p};
then (proj D).e in {p} by FUNCT_1:def 7;
then (proj D).e = p by TARSKI:def 1;
hence e in p by A2,Def9;
end;
theorem
for D being non empty a_partition of X, A being Subset of D
holds (proj D)"A = union A
proof
let D be non empty a_partition of X, A be Subset of D;
thus (proj D)"A c= union A
proof
let e be object;
assume e in (proj D)"A;
then (proj D).e in A & e in (proj D).e by Def9,FUNCT_2:38;
hence thesis by TARSKI:def 4;
end;
let e be object;
assume e in union A;
then consider u being set such that
A1: e in u and
A2: u in A by TARSKI:def 4;
A3: u in D by A2;
then (proj D).e = u by A1,Th65;
hence thesis by A1,A2,A3,FUNCT_2:38;
end;
theorem
for D being non empty a_partition of X, W being Element of D
ex W9 being Element of X st proj(D).W9=W
proof
let D be non empty a_partition of X, W be Element of D;
reconsider p = W as Subset of X;
p <> {} by Def4;
then consider W9 being Element of X such that
A1: W9 in p by SUBSET_1:4;
take W9;
thus thesis by A1,Th65;
end;
theorem
for D being non empty a_partition of X, W being Subset of X st
for B being Subset of X st B in D & B meets W holds B c= W holds W = proj D " (
proj D .: W)
proof
let D be non empty a_partition of X, W be Subset of X such that
A1: for B being Subset of X st B in D & B meets W holds B c= W;
W c= X;
then W c= dom proj D by FUNCT_2:def 1;
hence W c= proj D " (proj D .: W) by FUNCT_1:76;
let e be object;
assume
A2: e in proj D " (proj D .: W);
then reconsider d = e as Element of X;
(proj D).e in proj D .: W by A2,FUNCT_1:def 7;
then consider c being Element of X such that
A3: c in W and
A4: (proj D).d = (proj D).c by FUNCT_2:65;
reconsider B = (proj D).c as Subset of X by TARSKI:def 3;
c in (proj D).c by Def9;
then B meets W by A3,XBOOLE_0:3;
then
A5: B c= W by A1;
d in B by A4,Def9;
hence thesis by A5;
end;
theorem
for X being set, P being a_partition of X, x, a, b being set st
x in a & a in P & x in b & b in P holds a = b by Def4,XBOOLE_0:3;