--- a/src/HOL/Equiv_Relations.thy Mon Oct 25 23:10:06 2021 +0200
+++ b/src/HOL/Equiv_Relations.thy Tue Oct 26 11:15:40 2021 +0100
@@ -82,6 +82,9 @@
lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r"
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
+lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
+ by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
+
subsection \<open>Quotients\<close>