2.9 Quotients and Equivalence Classes
Equivalence Classes
Lemma
(1) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $R(s, t) ⇒ cl(t) ⊆ cl(s)$.
lemma class_relate_lem_a
(s t : X) (R : bin_rel X) (h : equivalence R) : R s t → cls R t ⊆ cls R s :=
Proof
QED.
Given that $R$ is an equivalence relation, we know that it is reflexive, symmetric and transitive.
rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R
⊢ R s t → cls R t ⊆ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s t → cls R t ⊆ cls R s
Thus, given an element $x$ in $cl(t)$ (i.e. $R(t, x)$ is true), we have, by transitivit, $R(s, x)$.
intros ha x hb,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s t → cls R t ⊆ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t
⊢ x ∈ cls R s
have hc : R t x := hb,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R t x
⊢ x ∈ cls R s
replace hc : R s t ∧ R t x, by {split, repeat {assumption}},
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R t x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s t ∧ R t x
⊢ x ∈ cls R s
replace hc : R s x := htrans s t x hc,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s t ∧ R t x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
Hence $x ∈ cl(s)$ by definition.
from hc
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
With lemma (1) in place, it is quite easy to see that, not only is $cl(t) ⊆ cl(s)$, in fact, $cl(t) = cl(s)$.
Lemma
(2) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $R(s, t) ⇒ cl(t) = cl(s)$.
lemma class_relate_lem_b
(s t : X) (R : bin_rel X) (h : equivalence R) : R s t → cls R t = cls R s :=
Proof
QED.
By lemma (1), $cl(t) ⊆ cl(s), and thus, we only need to prove that $cl(s) ⊆ cl(t)$ in order for $cl(t) = cl(s)$.
intro h0,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R
⊢ R s t → cls R t = cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t = cls R s
rw le_antisymm_iff,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t = cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s ∧ cls R s ≤ cls R t
split,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s ∧ cls R s ≤ cls R t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R s ≤ cls R t
all_goals {apply class_relate_lem_a,
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R s ≤ cls R t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
repeat {assumption}
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
},
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R t s
But, since $R$ is and equivalence relation, it is symmetric.
{rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R t s
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
Hence, $R(s, t) ↔ R(t, s)$ which by lemma (1) implies $cl(s) ⊆ cl(t)$ as required.
from hsym s t h0
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
}
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
no goals
Lemma
(3) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $¬ R(s, t) ⇒ cl(t) ∩ cl(s) = ∅$.
lemma class_not_relate
(s t : X) (R : bin_rel X) (h : equivalence R) : ¬ R s t → cls R t ∩ cls R s = ∅ :=
Proof
QED.
LEAN saying "cls R t ∩ cls R s = ∅" not decidable :/
have : (cls R t ∩ cls R s = ∅) ↔ ¬ ¬ (cls R t ∩ cls R s = ∅), rwa classical.not_not, rw this,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R
⊢ ¬R s t → cls R t ∩ cls R s = ∅
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅
⊢ ¬R s t → ¬¬cls R t ∩ cls R s = ∅
We prove by contradiction. Suppose $cl(t) ∩ cl(s) ≠ ∅$.
intros ha hb,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅
⊢ ¬R s t → ¬¬cls R t ∩ cls R s = ∅
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅
⊢ false
Then, there must be some $x$ in $cl(t) ∩ cl(s)$.
have hx : ∃ x, x ∈ cls R t ∩ cls R s := set.exists_mem_of_ne_empty hb,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
hx : ∃ (x : X), x ∈ cls R t ∩ cls R s
⊢ false
rcases hx with ⟨x, ⟨hα, hβ⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
hx : ∃ (x : X), x ∈ cls R t ∩ cls R s
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s
⊢ false
Thus, by definition, $R(t, x)$ and $R(s, t)$ must both be true!
rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ false
have hc : R s x ∧ R x t, by {split,
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ false
2 goals
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s x
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
from hβ,
2 goals
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s x
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
apply hsym, from hα},
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t
⊢ false
But this means $R(s, t)$ must also be true by transitivity, a contradiction to $¬ R(s, t)$!
have hd : R s t, by {from htrans s x t hc},
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t,
hd : R s t
⊢ false
contradiction,
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t,
hd : R s t
⊢ false
no goals
We now formally define a partition of a set $X$
Partition of a set $X$ is a set $A$ of non-empty subsets of $X$ with the property that each element of $X$ is in exacctly one of the subsets.
Theorem
Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then the set $V$ of equivalence classes $\{cl(s) | s ∈ X\}$ for $R$ is a partition of $X$.
theorem equiv_relation_partition -- or replace the set with (set.range (cls R))
(R : bin_rel X) (h : equivalence R) : partition {a : set X | ∃ s : X, a = cls R s} :=
Proof
QED.
To show that the equivalence classes of $R$ form a partition of $X$, we need to show that every $x ∈ X$ is in exactly one equivalence class of $R$, AND, none of the equivalence classes are empty.
split,
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ partition {a : set X | ∃ (s : X), a = cls R s}
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∀ (x : X),
∃ (B : set X) (H : B ∈ {a : set X | ∃ (s : X), a = cls R s}),
x ∈ B ∧ ∀ (C : set X), C ∈ {a : set X | ∃ (s : X), a = cls R s} → x ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
So let's first show that every $x ∈ X$ is in exactly one equivalence class of $R$. Let $y$ be and element of $X$.
{simp, intro y,
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∀ (x : X),
∃ (B : set X) (H : B ∈ {a : set X | ∃ (s : X), a = cls R s}),
x ∈ B ∧ ∀ (C : set X), C ∈ {a : set X | ∃ (s : X), a = cls R s} → x ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (B : set X),
(∃ (s : X), B = cls R s) ∧ y ∈ B ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → B = C
existsi cls R y,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (B : set X),
(∃ (s : X), B = cls R s) ∧ y ∈ B ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ (∃ (s : X), cls R y = cls R s) ∧
y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
split,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ (∃ (s : X), cls R y = cls R s) ∧
y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (s : X), cls R y = cls R s
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
Then obviously $y ∈ cl(y)$ since $R(y, y)$ is true by reflexivity.
{use y},
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (s : X), cls R y = cls R s
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
{split,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
{from itself_in_cls R h y},
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
Okay. So now we need to prove uniqueness. Suppose there is a $x ∈ X$, $x ∈ cl(y)$, we then need to show $cl(y) = cl(x)$.
{intros C x hC hy_in_C, rw hC,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ cls R y = cls R x
But this is true by lemma (2)!
apply class_relate_lem_b, assumption,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ cls R y = cls R x
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ R x y
have : y ∈ cls R x, rwa ←hC,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ R x y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ cls R x
⊢ R x y
unfold cls at this,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ cls R x
⊢ R x y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ {x_1 : X | R x x_1}
⊢ R x y
rwa set.mem_set_of_eq at this}
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ {x_1 : X | R x x_1}
⊢ R x y
no goals
}
no goals
no goals
},
no goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
Now we have to prove that none of the equivalence classes are empty. But this is quite simple. Suppose there is an equivalence class $cl(x)$ where $x ∈ X$ that is empty.
{simp, intros x hx,
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : ∅ = cls R x
⊢ false
But then $x ∈ cl(x)$ as $R(x, x)$ is true by reflexivity. Ah ha! Contradiction! Hence, such empty equivalence class does not in fact exist! And we are done.
rw set.empty_def at hx,
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : ∅ = cls R x
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x
⊢ false
have : x ∈ {x : X | false}, by {rw hx, from itself_in_cls R h x},
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
rwa set.mem_set_of_eq at this
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
}
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
no goals
Theorem
Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then any partition of $X$ can form a equivalence relation.
theorem partition_equiv_relation -- I have defined rs to be: def rs (A : set (set(X))) (s t : X) := ∃ B ∈ A, s ∈ B ∧ t ∈ B
(C : set (set(X))) (h : partition C) : equivalence (rs C) :=
Proof
QED.
Proving reflexivity
{intro x,
2 goals
X : Type u,
C : set (set X),
h : partition C
⊢ reflexive (rs C)
X : Type u,
C : set (set X),
h : partition C
⊢ symmetric (rs C) ∧ transitive (rs C)
X : Type u,
C : set (set X),
h : partition C,
x : X
⊢ rs C x x
cases h with ha hb,
X : Type u,
C : set (set X),
h : partition C,
x : X
⊢ rs C x x
X : Type u,
C : set (set X),
x : X,
ha : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hb : ∅ ∉ C
⊢ rs C x x
replace ha :
X : Type u,
C : set (set X),
x : X,
ha : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hb : ∅ ∉ C
⊢ rs C x x
X : Type u,
C : set (set X),
x : X,
ha : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hb : ∅ ∉ C
⊢ rs C x x
∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (D : set X), D ∈ C → x ∈ D → B = D := ha x,
X : Type u,
C : set (set X),
x : X,
ha : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hb : ∅ ∉ C
⊢ rs C x x
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (D : set X), D ∈ C → x ∈ D → B = D
⊢ rs C x x
rcases ha with ⟨ha, ⟨hb, ⟨hc, hd⟩⟩⟩,
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (D : set X), D ∈ C → x ∈ D → B = D
⊢ rs C x x
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ rs C x x
use ha, use hb,
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ rs C x x
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha ∧ x ∈ ha
split,
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha ∧ x ∈ ha
2 goals
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
repeat {assumption}
2 goals
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
2 goals
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
},
2 goals
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
X : Type u,
C : set (set X),
x : X,
hb : ∅ ∉ C,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : ∀ (D : set X), D ∈ C → x ∈ D → ha = D
⊢ x ∈ ha
X : Type u,
C : set (set X),
h : partition C
⊢ symmetric (rs C) ∧ transitive (rs C)
Proving symmtric
{split,
X : Type u,
C : set (set X),
h : partition C
⊢ symmetric (rs C) ∧ transitive (rs C)
2 goals
X : Type u,
C : set (set X),
h : partition C
⊢ symmetric (rs C)
X : Type u,
C : set (set X),
h : partition C
⊢ transitive (rs C)
{rintros x y ⟨ha, ⟨hb, ⟨hc, hd⟩⟩⟩,
2 goals
X : Type u,
C : set (set X),
h : partition C
⊢ symmetric (rs C)
X : Type u,
C : set (set X),
h : partition C
⊢ transitive (rs C)
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ rs C y x
use ha, use hb,
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ rs C y x
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha ∧ x ∈ ha
split,
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha ∧ x ∈ ha
2 goals
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ x ∈ ha
repeat {assumption}
2 goals
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ x ∈ ha
2 goals
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ x ∈ ha
},
2 goals
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ y ∈ ha
X : Type u,
C : set (set X),
h : partition C,
x y : X,
ha : set X,
hb : ha ∈ C,
hc : x ∈ ha,
hd : y ∈ ha
⊢ x ∈ ha
X : Type u,
C : set (set X),
h : partition C
⊢ transitive (rs C)
Proving transitive
{rintros x y z ⟨⟨ha, ⟨hb, ⟨hd, he⟩⟩⟩, ⟨hf, ⟨hg, ⟨hk, hl⟩⟩⟩⟩,
X : Type u,
C : set (set X),
h : partition C
⊢ transitive (rs C)
X : Type u,
C : set (set X),
h : partition C,
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf
⊢ rs C x z
use ha, use hb,
X : Type u,
C : set (set X),
h : partition C,
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf
⊢ rs C x z
X : Type u,
C : set (set X),
h : partition C,
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf
⊢ x ∈ ha ∧ z ∈ ha
cases h with hm hn,
X : Type u,
C : set (set X),
h : partition C,
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf
⊢ x ∈ ha ∧ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hm : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hn : ∅ ∉ C
⊢ x ∈ ha ∧ z ∈ ha
replace hm :
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hm : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hn : ∅ ∉ C
⊢ x ∈ ha ∧ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hm : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hn : ∅ ∉ C
⊢ x ∈ ha ∧ z ∈ ha
∃ (B : set X) (H : B ∈ C), y ∈ B ∧ ∀ (D : set X), D ∈ C → y ∈ D → B = D := hm y,
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hm : ∀ (x : X), ∃ (B : set X) (H : B ∈ C), x ∈ B ∧ ∀ (C_1 : set X), C_1 ∈ C → x ∈ C_1 → B = C_1,
hn : ∅ ∉ C
⊢ x ∈ ha ∧ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
hm : ∃ (B : set X) (H : B ∈ C), y ∈ B ∧ ∀ (D : set X), D ∈ C → y ∈ D → B = D
⊢ x ∈ ha ∧ z ∈ ha
rcases hm with ⟨ho, ⟨hp, ⟨hq, hr⟩⟩⟩,
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
hm : ∃ (B : set X) (H : B ∈ C), y ∈ B ∧ ∀ (D : set X), D ∈ C → y ∈ D → B = D
⊢ x ∈ ha ∧ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ x ∈ ha ∧ z ∈ ha
have : hf = ha,
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ x ∈ ha ∧ z ∈ ha
2 goals
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ hf = ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha ∧ z ∈ ha
{suffices : hf = ho, {rw this, apply hr ha, repeat {assumption}},
2 goals
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ hf = ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha ∧ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ hf = ho
rwa hr hf, repeat {assumption},
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D
⊢ hf = ho
no goals
},
no goals
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha ∧ z ∈ ha
split,
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha ∧ z ∈ ha
2 goals
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ z ∈ ha
{assumption},
2 goals
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ x ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ z ∈ ha
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ z ∈ ha
{rwa ←this},
X : Type u,
C : set (set X),
x y z : X,
ha : set X,
hb : ha ∈ C,
hd : x ∈ ha,
he : y ∈ ha,
hf : set X,
hg : hf ∈ C,
hk : y ∈ hf,
hl : z ∈ hf,
hn : ∅ ∉ C,
ho : set X,
hp : ho ∈ C,
hq : y ∈ ho,
hr : ∀ (D : set X), D ∈ C → y ∈ D → ho = D,
this : hf = ha
⊢ z ∈ ha
no goals
}
no goals
no goals
}
no goals
no goals