section ‹Systems of Representatives of Equivalence Relations›
theory Representative_System
imports Main
begin
definition repsys :: "'a set ⇒ 'a rel ⇒ 'a set"
where
"repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
text ‹Equivalence classes of an equivalence relation are nonempty.›
lemma class_nonempty:
assumes "equiv A R" and "X ∈ A // R"
shows "∃x. x ∈ X"
using assms by (metis equiv_class_self quotientE)
lemma repsys_subset:
assumes "equiv A R"
shows "repsys A R ⊆ A"
using class_nonempty [OF assms]
by (auto simp: repsys_def) (metis UnionI Union_quotient assms someI_ex)
lemma mem_repsys_class:
assumes "equiv A R" and "x ∈ repsys A R"
shows "∃X ∈ A // R. x ∈ X"
using class_nonempty [OF assms(1)] and assms(2)
by (auto simp: repsys_def) (metis someI_ex)
lemma repsys_unique_modulo:
assumes "equiv A R"
and "x ∈ repsys A R" and "y ∈ repsys A R" and "x ≠ y"
shows "(x, y) ∉ R"
using assms by (auto simp: repsys_def) (metis (lifting) class_nonempty quotient_eq_iff someI_ex)
lemma repsys_representative:
assumes "equiv A R"
and "x ∈ A"
shows "∃y ∈ repsys A R. (x, y) ∈ R"
proof -
from Union_quotient [OF assms(1)] and ‹x ∈ A› obtain X
where "X ∈ A // R" and "x ∈ X" by auto
then have "(x, (SOME x. x ∈ X)) ∈ R"
using quotient_eq_iff [OF assms(1)] by (metis someI_ex)
moreover have "(SOME x. x ∈ X) ∈ repsys A R"
using ‹X ∈ A // R› by (auto simp: repsys_def)
ultimately show ?thesis by blast
qed
end