English
For a setoid s on α, the quotient is a singleton (subsingleton) if and only if s is the universal relation ⊤.
Русский
Чему-то относится: фактор-приложение по отношению s является единичным (одиночным) тогда и только тогда, когда s — тождественная тождественность, т. е. ⊤.
LaTeX
$$$\\operatorname{Subsingleton}(\\operatorname{Quotient} s) \\iff s = \\top.$$$
Lean4
@[simp]
theorem subsingleton_iff {s : Setoid α} : Subsingleton (Quotient s) ↔ s = ⊤ :=
by
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)
simp_rw [«Prop».top_eq_true, true_implies, Quotient.eq']
