English
For any relation r on α, Subsingleton(Quotient r) holds if and only if the generated equivalence relation EqvGen r is the universal relation ⊤.
Русский
Для любой relation r на α: Subsingleton(Quot r) эквивалентно EqvGen r = ⊤.
LaTeX
$$$\\operatorname{Subsingleton}(\\operatorname{Quotient} r) \\iff \\operatorname{EqvGen} r = \\top.$$$
Lean4
theorem subsingleton_iff (r : α → α → Prop) : Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤ :=
by
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]
refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)
refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)
rw [Quot.eq]
simp only [forall_const, le_Prop_eq, «Prop».top_eq_true]
