section ‹Equivalence relations›
theory EquivClass1 imports ZF.EquivClass func_ZF ZF1
begin
text‹In this theory file we extend the work on equivalence relations
done in the standard Isabelle's EquivClass theory. That development
is very good and all, but we really would prefer an approach contained within
the a standard ZF set theory, without extensions specific to Isabelle.
That is why this theory is written.
›
subsection‹Congruent functions and projections on the quotient›
text‹Suppose we have a set $X$ with a relation
$r\subseteq X\times X$ and a function $f: X\rightarrow X$.
The function $f$ can be compatible (congruent) with $r$ in the sense that
if two elements $x,y$ are related then the values $f(x), f(x)$
are also related. This is especially useful if $r$ is an
equivalence relation as it allows to "project" the function
to the quotient space $X/r$ (the set of equivalence classes of $r$)
and create a new function $F$ that satifies the formula
$F([x]_r) = [f(x)]_r$. When $f$ is congruent with respect
to $r$ such definition of the value of $F$ on the equivalence class
$[x]_r$ does not depend on which $x$ we choose to represent the class.
In this section we also consider binary operations that are congruent
with respect to a relation. These are important in algebra - the
congruency condition allows to project the operation
to obtain the operation on the quotient space.
›
text‹First we define the notion of function that maps equivalent
elements to equivalent values. We use similar names as
in the Isabelle's standard ‹EquivClass› theory to indicate
the conceptual correspondence of the notions.›
definition
"Congruent(r,f) ≡
(∀x y. ⟨x,y⟩ ∈ r ⟶ ⟨f`(x),f`(y)⟩ ∈ r)"
text‹Now we will define the projection of
a function onto the quotient space. In standard math the equivalence class
of $x$ with respect to relation $r$ is usually denoted $[x]_r$. Here we reuse
notation $r\{ x\}$ instead. This means the image of the set $\{ x\}$
with respect to the relation, which, for equivalence relations is
exactly its equivalence class if you think about it.›
definition
"ProjFun(A,r,f) ≡
{⟨c,⋃x∈c. r``{f`(x)}⟩. c ∈ (A//r)}"
text‹Elements of equivalence classes belong to the set.›
lemma EquivClass_1_L1:
assumes A1: "equiv(A,r)" and A2: "C ∈ A//r" and A3: "x∈C"
shows "x∈A"
proof -
from A2 have "C ⊆ ⋃ (A//r)" by auto
with A1 A3 show "x∈A"
using Union_quotient by auto
qed
text‹The image of a subset of $X$ under projection is a subset
of $A/r$.›
lemma EquivClass_1_L1A:
assumes "A⊆X" shows "{r``{x}. x∈A} ⊆ X//r"
using assms quotientI by auto
text‹If an element belongs to an equivalence class, then its image
under relation is this equivalence class.›
lemma EquivClass_1_L2:
assumes A1: "equiv(A,r)" "C ∈ A//r" and A2: "x∈C"
shows "r``{x} = C"
proof -
from A1 A2 have "x ∈ r``{x}"
using EquivClass_1_L1 equiv_class_self by simp
with A2 have I: "r``{x}∩C ≠ 0" by auto
from A1 A2 have "r``{x} ∈ A//r"
using EquivClass_1_L1 quotientI by simp
with A1 I show ?thesis
using quotient_disj by blast
qed
text‹Elements that belong to the same equivalence class are equivalent.›
lemma EquivClass_1_L2A:
assumes "equiv(A,r)" "C ∈ A//r" "x∈C" "y∈C"
shows "⟨x,y⟩ ∈ r"
using assms EquivClass_1_L2 EquivClass_1_L1 equiv_class_eq_iff
by simp
text‹Every $x$ is in the class of $y$, then they are equivalent.›
lemma EquivClass_1_L2B:
assumes A1: "equiv(A,r)" and A2: "y∈A" and A3: "x ∈ r``{y}"
shows "⟨x,y⟩ ∈ r"
proof -
from A2 have "r``{y} ∈ A//r"
using quotientI by simp
with A1 A3 show ?thesis using
EquivClass_1_L1 equiv_class_self equiv_class_nondisjoint by blast
qed
text‹If a function is congruent then the equivalence classes of the values
that come from the arguments from the same class are the same.›
lemma EquivClass_1_L3:
assumes A1: "equiv(A,r)" and A2: "Congruent(r,f)"
and A3: "C ∈ A//r" "x∈C" "y∈C"
shows "r``{f`(x)} = r``{f`(y)}"
proof -
from A1 A3 have "⟨x,y⟩ ∈ r"
using EquivClass_1_L2A by simp
with A2 have "⟨f`(x),f`(y)⟩ ∈ r"
using Congruent_def by simp
with A1 show ?thesis using equiv_class_eq by simp
qed
text‹The values of congruent functions are in the space.›
lemma EquivClass_1_L4:
assumes A1: "equiv(A,r)" and A2: "C ∈ A//r" "x∈C"
and A3: "Congruent(r,f)"
shows "f`(x) ∈ A"
proof -
from A1 A2 have "x∈A"
using EquivClass_1_L1 by simp
with A1 have "⟨x,x⟩ ∈ r"
using equiv_def refl_def by simp
with A3 have "⟨f`(x),f`(x)⟩ ∈ r"
using Congruent_def by simp
with A1 show ?thesis using equiv_type by auto
qed
text‹Equivalence classes are not empty.›
lemma EquivClass_1_L5:
assumes A1: "refl(A,r)" and A2: "C ∈ A//r"
shows "C≠0"
proof -
from A2 obtain x where I: "C = r``{x}" and "x∈A"
using quotient_def by auto
from A1 ‹x∈A› have "x ∈ r``{x}" using refl_def by auto
with I show ?thesis by auto
qed
text‹To avoid using an axiom of choice, we define the projection using
the expression $\bigcup _{x\in C} r(\{f(x)\})$.
The next lemma shows that for
congruent function this is in the quotient space $A/r$.›
lemma EquivClass_1_L6:
assumes A1: "equiv(A,r)" and A2: "Congruent(r,f)"
and A3: "C ∈ A//r"
shows "(⋃x∈C. r``{f`(x)}) ∈ A//r"
proof -
from A1 have "refl(A,r)" unfolding equiv_def by simp
with A3 have "C≠0" using EquivClass_1_L5 by simp
moreover from A2 A3 A1 have "∀x∈C. r``{f`(x)} ∈ A//r"
using EquivClass_1_L4 quotientI by auto
moreover from A1 A2 A3 have
"∀x y. x∈C ∧ y∈C ⟶ r``{f`(x)} = r``{f`(y)}"
using EquivClass_1_L3 by blast
ultimately show ?thesis by (rule ZF1_1_L2)
qed
text‹Congruent functions can be projected.›
lemma EquivClass_1_T0:
assumes "equiv(A,r)" "Congruent(r,f)"
shows "ProjFun(A,r,f) : A//r → A//r"
using assms EquivClass_1_L6 ProjFun_def ZF_fun_from_total
by simp
text‹We now define congruent functions of two variables (binary funtions).
The predicate ‹Congruent2› corresponds to ‹congruent2›
in Isabelle's standard ‹EquivClass› theory,
but uses ZF-functions rather than meta-functions.›
definition
"Congruent2(r,f) ≡
(∀x⇩1 x⇩2 y⇩1 y⇩2. ⟨x⇩1,x⇩2⟩ ∈ r ∧ ⟨y⇩1,y⇩2⟩ ∈ r ⟶
⟨f`⟨x⇩1,y⇩1⟩, f`⟨x⇩2,y⇩2⟩ ⟩ ∈ r)"
text‹Next we define the notion of projecting a binary operation
to the quotient space. This is a very important concept that
allows to define quotient groups, among other things.›
definition
"ProjFun2(A,r,f) ≡
{⟨p,⋃ z ∈ fst(p)×snd(p). r``{f`(z)}⟩. p ∈ (A//r)×(A//r) }"
text‹The following lemma is a two-variables equivalent
of ‹EquivClass_1_L3›.›
lemma EquivClass_1_L7:
assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "C⇩1 ∈ A//r" "C⇩2 ∈ A//r"
and A4: "z⇩1 ∈ C⇩1×C⇩2" "z⇩2 ∈ C⇩1×C⇩2"
shows "r``{f`(z⇩1)} = r``{f`(z⇩2)}"
proof -
from A4 obtain x⇩1 y⇩1 x⇩2 y⇩2 where
"x⇩1∈C⇩1" and "y⇩1∈C⇩2" and "z⇩1 = ⟨x⇩1,y⇩1⟩" and
"x⇩2∈C⇩1" and "y⇩2∈C⇩2" and "z⇩2 = ⟨x⇩2,y⇩2⟩"
by auto
with A1 A3 have "⟨x⇩1,x⇩2⟩ ∈ r" and "⟨y⇩1,y⇩2⟩ ∈ r"
using EquivClass_1_L2A by auto
with A2 have "⟨f`⟨x⇩1,y⇩1⟩,f`⟨x⇩2,y⇩2⟩⟩ ∈ r"
using Congruent2_def by simp
with A1 ‹z⇩1 = ⟨x⇩1,y⇩1⟩› ‹z⇩2 = ⟨x⇩2,y⇩2⟩› show ?thesis
using equiv_class_eq by simp
qed
text‹The values of congruent functions of two variables are in the space.›
lemma EquivClass_1_L8:
assumes A1: "equiv(A,r)" and A2: "C⇩1 ∈ A//r" and A3: "C⇩2 ∈ A//r"
and A4: "z ∈ C⇩1×C⇩2" and A5: "Congruent2(r,f)"
shows "f`(z) ∈ A"
proof -
from A4 obtain x y where "x∈C⇩1" and "y∈C⇩2" and "z = ⟨x,y⟩"
by auto
with A1 A2 A3 have "x∈A" and "y∈A"
using EquivClass_1_L1 by auto
with A1 A4 have "⟨x,x⟩ ∈ r" and "⟨y,y⟩ ∈ r"
using equiv_def refl_def by auto
with A5 have "⟨f`⟨x,y⟩, f`⟨x,y⟩ ⟩ ∈ r"
using Congruent2_def by simp
with A1 ‹z = ⟨x,y⟩› show ?thesis using equiv_type by auto
qed
text‹The values of congruent functions are in the space. Note that
although this lemma is intended to be used with functions, we don't
need to assume that $f$ is a function.›
lemma EquivClass_1_L8A:
assumes A1: "equiv(A,r)" and A2: "x∈A" "y∈A"
and A3: "Congruent2(r,f)"
shows "f`⟨x,y⟩ ∈ A"
proof -
from A1 A2 have "r``{x} ∈ A//r" "r``{y} ∈ A//r"
"⟨x,y⟩ ∈ r``{x}×r``{y}"
using equiv_class_self quotientI by auto
with A1 A3 show ?thesis using EquivClass_1_L8 by simp
qed
text‹The following lemma is a two-variables equivalent of
‹EquivClass_1_L6›.›
lemma EquivClass_1_L9:
assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "p ∈ (A//r)×(A//r)"
shows "(⋃ z ∈ fst(p)×snd(p). r``{f`(z)}) ∈ A//r"
proof -
from A3 have "fst(p) ∈ A//r" and "snd(p) ∈ A//r"
by auto
with A1 A2 have
I: "∀z ∈ fst(p)×snd(p). f`(z) ∈ A"
using EquivClass_1_L8 by simp
from A3 A1 have "fst(p)×snd(p) ≠ 0"
using equiv_def EquivClass_1_L5 Sigma_empty_iff
by auto
moreover from A1 I have
"∀z ∈ fst(p)×snd(p). r``{f`(z)} ∈ A//r"
using quotientI by simp
moreover from A1 A2 ‹fst(p) ∈ A//r› ‹snd(p) ∈ A//r› have
"∀z⇩1 z⇩2. z⇩1 ∈ fst(p)×snd(p) ∧ z⇩2 ∈ fst(p)×snd(p) ⟶
r``{f`(z⇩1)} = r``{f`(z⇩2)}"
using EquivClass_1_L7 by blast
ultimately show ?thesis by (rule ZF1_1_L2)
qed
text‹Congruent functions of two variables can be projected.›
theorem EquivClass_1_T1:
assumes "equiv(A,r)" "Congruent2(r,f)"
shows "ProjFun2(A,r,f) : (A//r)×(A//r) → A//r"
using assms EquivClass_1_L9 ProjFun2_def ZF_fun_from_total
by simp
text‹The projection diagram commutes. I wish I knew how to draw this diagram
in LaTeX.›
lemma EquivClass_1_L10:
assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "x∈A" "y∈A"
shows "ProjFun2(A,r,f)`⟨r``{x},r``{y}⟩ = r``{f`⟨x,y⟩}"
proof -
from A3 A1 have "r``{x} × r``{y} ≠ 0"
using quotientI equiv_def EquivClass_1_L5 Sigma_empty_iff
by auto
moreover have
"∀z ∈ r``{x}×r``{y}. r``{f`(z)} = r``{f`⟨x,y⟩}"
proof
fix z assume A4: "z ∈ r``{x}×r``{y}"
from A1 A3 have
"r``{x} ∈ A//r" "r``{y} ∈ A//r"
"⟨x,y⟩ ∈ r``{x}×r``{y}"
using quotientI equiv_class_self by auto
with A1 A2 A4 show
"r``{f`(z)} = r``{f`⟨x,y⟩}"
using EquivClass_1_L7 by blast
qed
ultimately have
"(⋃z ∈ r``{x}×r``{y}. r``{f`(z)}) = r``{f`⟨x,y⟩}"
by (rule ZF1_1_L1)
moreover have
"ProjFun2(A,r,f)`⟨r``{x},r``{y}⟩ = (⋃z ∈ r``{x}×r``{y}. r``{f`(z)})"
proof -
from assms have
"ProjFun2(A,r,f) : (A//r)×(A//r) → A//r"
"⟨r``{x},r``{y}⟩ ∈ (A//r)×(A//r)"
using EquivClass_1_T1 quotientI by auto
then show ?thesis using ProjFun2_def ZF_fun_from_tot_val
by auto
qed
ultimately show ?thesis by simp
qed
subsection‹Projecting commutative, associative and distributive operations.›
text‹In this section we show that if the operations are congruent with
respect to an equivalence relation then the projection to the quotient
space preserves commutativity, associativity and distributivity.›
text‹The projection of commutative operation is commutative.›
lemma EquivClass_2_L1: assumes
A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "f {is commutative on} A"
and A4: "c1 ∈ A//r" "c2 ∈ A//r"
shows "ProjFun2(A,r,f)`⟨c1,c2⟩ = ProjFun2(A,r,f)`⟨c2,c1⟩"
proof -
from A4 obtain x y where D1:
"c1 = r``{x}" "c2 = r``{y}"
"x∈A" "y∈A"
using quotient_def by auto
with A1 A2 have "ProjFun2(A,r,f)`⟨c1,c2⟩ = r``{f`⟨x,y⟩}"
using EquivClass_1_L10 by simp
also from A3 D1 have
"r``{f`⟨x,y⟩} = r``{f`⟨y,x⟩}"
using IsCommutative_def by simp
also from A1 A2 D1 have
"r``{f`⟨y,x⟩} = ProjFun2(A,r,f)` ⟨c2,c1⟩"
using EquivClass_1_L10 by simp
finally show ?thesis by simp
qed
text‹The projection of commutative operation is commutative.›
theorem EquivClass_2_T1:
assumes "equiv(A,r)" and "Congruent2(r,f)"
and "f {is commutative on} A"
shows "ProjFun2(A,r,f) {is commutative on} A//r"
using assms IsCommutative_def EquivClass_2_L1 by simp
text‹The projection of an associative operation is associative.›
lemma EquivClass_2_L2:
assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "f {is associative on} A"
and A4: "c1 ∈ A//r" "c2 ∈ A//r" "c3 ∈ A//r"
and A5: "g = ProjFun2(A,r,f)"
shows "g`⟨g`⟨c1,c2⟩,c3⟩ = g`⟨c1,g`⟨c2,c3⟩⟩"
proof -
from A4 obtain x y z where D1:
"c1 = r``{x}" "c2 = r``{y}" "c3 = r``{z}"
"x∈A" "y∈A" "z∈A"
using quotient_def by auto
with A3 have T1:"f`⟨x,y⟩ ∈ A" "f`⟨y,z⟩ ∈ A"
using IsAssociative_def apply_type by auto
with A1 A2 D1 A5 have
"g`⟨g`⟨c1,c2⟩,c3⟩ = r``{f`⟨f`⟨x,y⟩,z⟩}"
using EquivClass_1_L10 by simp
also from D1 A3 have
"… = r``{f`⟨x,f`⟨y,z⟩ ⟩}"
using IsAssociative_def by simp
also from T1 A1 A2 D1 A5 have
"… = g`⟨c1,g`⟨c2,c3⟩⟩"
using EquivClass_1_L10 by simp
finally show ?thesis by simp
qed
text‹The projection of an associative operation is associative on the
quotient.›
theorem EquivClass_2_T2:
assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
and A3: "f {is associative on} A"
shows "ProjFun2(A,r,f) {is associative on} A//r"
proof -
let ?g = "ProjFun2(A,r,f)"
from A1 A2 have
"?g ∈ (A//r)×(A//r) → A//r"
using EquivClass_1_T1 by simp
moreover from A1 A2 A3 have
"∀c1 ∈ A//r.∀c2 ∈ A//r.∀c3 ∈ A//r.
?g`⟨?g`⟨c1,c2⟩,c3⟩ = ?g`⟨c1,?g`⟨c2,c3⟩⟩"
using EquivClass_2_L2 by simp
ultimately show ?thesis
using IsAssociative_def by simp
qed
text‹The essential condition to show that distributivity is preserved by
projections to quotient spaces, provided both operations are congruent
with respect to the equivalence relation.›
lemma EquivClass_2_L3:
assumes A1: "IsDistributive(X,A,M)"
and A2: "equiv(X,r)"
and A3: "Congruent2(r,A)" "Congruent2(r,M)"
and A4: "a ∈ X//r" "b ∈ X//r" "c ∈ X//r"
and A5: "A⇩p = ProjFun2(X,r,A)" "M⇩p = ProjFun2(X,r,M)"
shows "M⇩p`⟨a,A⇩p`⟨b,c⟩⟩ = A⇩p`⟨ M⇩p`⟨a,b⟩,M⇩p`⟨a,c⟩⟩ ∧
M⇩p`⟨ A⇩p`⟨b,c⟩,a ⟩ = A⇩p`⟨ M⇩p`⟨b,a⟩, M⇩p`⟨c,a⟩⟩"
proof
from A4 obtain x y z where "x∈X" "y∈X" "z∈X"
"a = r``{x}" "b = r``{y}" "c = r``{z}"
using quotient_def by auto
with A1 A2 A3 A5 show
"M⇩p`⟨a,A⇩p`⟨b,c⟩⟩ = A⇩p`⟨ M⇩p`⟨a,b⟩,M⇩p`⟨a,c⟩⟩" and
"M⇩p`⟨ A⇩p`⟨b,c⟩,a ⟩ = A⇩p`⟨ M⇩p`⟨b,a⟩, M⇩p`⟨c,a⟩⟩"
using EquivClass_1_L8A EquivClass_1_L10 IsDistributive_def
by auto
qed
text‹Distributivity is preserved by
projections to quotient spaces, provided both operations are congruent
with respect to the equivalence relation.›
lemma EquivClass_2_L4: assumes A1: "IsDistributive(X,A,M)"
and A2: "equiv(X,r)"
and A3: "Congruent2(r,A)" "Congruent2(r,M)"
shows "IsDistributive(X//r,ProjFun2(X,r,A),ProjFun2(X,r,M))"
proof-
let ?A⇩p = "ProjFun2(X,r,A)"
let ?M⇩p = "ProjFun2(X,r,M)"
from A1 A2 A3 have
"∀a∈X//r.∀b∈X//r.∀c∈X//r.
?M⇩p`⟨a,?A⇩p`⟨b,c⟩⟩ = ?A⇩p`⟨?M⇩p`⟨a,b⟩,?M⇩p`⟨a,c⟩⟩ ∧
?M⇩p`⟨?A⇩p`⟨b,c⟩,a⟩ = ?A⇩p`⟨?M⇩p`⟨b,a⟩,?M⇩p`⟨c,a⟩⟩"
using EquivClass_2_L3 by simp
then show ?thesis using IsDistributive_def by simp
qed
subsection‹Saturated sets›
text‹In this section we consider sets that are saturated
with respect to an equivalence
relation. A set $A$ is saturated with respect to a relation
$r$ if $A=r^{-1}(r(A))$.
For equivalence relations saturated sets are unions of equivalence classes.
This makes them useful as a tool to define subsets of
the quoutient space using properties
of representants. Namely, we often define a set
$B\subseteq X/r$ by saying that
$[x]_r \in B$ iff $x\in A$.
If $A$ is a saturated set, this definition is consistent in
the sense that it does not depend on the choice of $x$ to
represent $[x]_r$.›
text‹The following defines the notion of a saturated set.
Recall that in Isabelle
‹r-``(A)› is the inverse image of $A$ with respect to relation $r$.
This definition is not specific to equivalence relations.›
definition
"IsSaturated(r,A) ≡ A = r-``(r``(A))"
text‹For equivalence relations a set is saturated iff it is an image
of itself.›
lemma EquivClass_3_L1: assumes A1: "equiv(X,r)"
shows "IsSaturated(r,A) ⟷ A = r``(A)"
proof
assume "IsSaturated(r,A)"
then have "A = (converse(r) O r)``(A)"
using IsSaturated_def vimage_def image_comp
by simp
also from A1 have "… = r``(A)"
using equiv_comp_eq by simp
finally show "A = r``(A)" by simp
next assume "A = r``(A)"
with A1 have "A = (converse(r) O r)``(A)"
using equiv_comp_eq by simp
also have "… = r-``(r``(A))"
using vimage_def image_comp by simp
finally have "A = r-``(r``(A))" by simp
then show "IsSaturated(r,A)" using IsSaturated_def
by simp
qed
text‹For equivalence relations sets are contained in their images.›
lemma EquivClass_3_L2: assumes A1: "equiv(X,r)" and A2: "A⊆X"
shows "A ⊆ r``(A)"
proof
fix a assume "a∈A"
with A1 A2 have "a ∈ r``{a}"
using equiv_class_self by auto
with ‹a∈A› show "a ∈ r``(A)" by auto
qed
text‹The next lemma shows that if "$\sim$"
is an equivalence relation and a set
$A$ is such that $a\in A$ and $a\sim b$ implies $b\in A$, then
$A$ is saturated with respect to the relation.›
lemma EquivClass_3_L3: assumes A1: "equiv(X,r)"
and A2: "r ⊆ X×X" and A3: "A⊆X"
and A4: "∀x∈A. ∀y∈X. ⟨x,y⟩ ∈ r ⟶ y∈A"
shows "IsSaturated(r,A)"
proof -
from A2 A4 have "r``(A) ⊆ A"
using image_iff by blast
moreover from A1 A3 have "A ⊆ r``(A)"
using EquivClass_3_L2 by simp
ultimately have "A = r``(A)" by auto
with A1 show "IsSaturated(r,A)" using EquivClass_3_L1
by simp
qed
text‹If $A\subseteq X$ and $A$ is saturated and $x\sim y$, then $x\in A$ iff
$y\in A$. Here we show only one direction.›
lemma EquivClass_3_L4: assumes A1: "equiv(X,r)"
and A2: "IsSaturated(r,A)" and A3: "A⊆X"
and A4: "⟨x,y⟩ ∈ r"
and A5: "x∈X" "y∈A"
shows "x∈A"
proof -
from A1 A5 have "x ∈ r``{x}"
using equiv_class_self by simp
with A1 A3 A4 A5 have "x ∈ r``(A)"
using equiv_class_eq equiv_class_self
by auto
with A1 A2 show "x∈A"
using EquivClass_3_L1 by simp
qed
text‹If $A\subseteq X$ and $A$ is saturated and $x\sim y$, then $x\in A$ iff
$y\in A$.›
lemma EquivClass_3_L5: assumes A1: "equiv(X,r)"
and A2: "IsSaturated(r,A)" and A3: "A⊆X"
and A4: "x∈X" "y∈X"
and A5: "⟨x,y⟩ ∈ r"
shows "x∈A ⟷ y∈A"
proof
assume "y∈A"
with assms show "x∈A" using EquivClass_3_L4
by simp
next assume "x∈A"
from A1 A5 have "⟨y,x⟩ ∈ r"
using equiv_is_sym by blast
with A1 A2 A3 A4 ‹x∈A› show "y∈A"
using EquivClass_3_L4 by simp
qed
text‹If $A$ is saturated then $x\in A$ iff its class is in the projection
of $A$.›
lemma EquivClass_3_L6: assumes A1: "equiv(X,r)"
and A2: "IsSaturated(r,A)" and A3: "A⊆X" and A4: "x∈X"
and A5: "B = {r``{x}. x∈A}"
shows "x∈A ⟷ r``{x} ∈ B"
proof
assume "x∈A"
with A5 show "r``{x} ∈ B" by auto
next assume "r``{x} ∈ B"
with A5 obtain y where "y ∈ A" and "r``{x} = r``{y}"
by auto
with A1 A3 have "⟨x,y⟩ ∈ r"
using eq_equiv_class by auto
with A1 A2 A3 A4 ‹y ∈ A› show "x∈A"
using EquivClass_3_L4 by simp
qed
text‹A technical lemma involving a projection of a saturated set and a
logical epression with exclusive or. Note that we don't really care
what ‹Xor› is here, this is true for any predicate.›
lemma EquivClass_3_L7: assumes "equiv(X,r)"
and "IsSaturated(r,A)" and "A⊆X"
and "x∈X" "y∈X"
and "B = {r``{x}. x∈A}"
and "(x∈A) Xor (y∈A)"
shows "(r``{x} ∈ B) Xor (r``{y} ∈ B)"
using assms EquivClass_3_L6 by simp
end