unique_quotient_iff_eq_top — Mathlib

English

There exists a nonempty unique structure on M / p if and only if p = ⊤.

Русский

Существует не пустая уникальная структура на фактор-модуле M / p тогда и только тогда, когда p = ⊤.

LaTeX

$$$$ \\text{Nonempty } (\\text{Unique}(M / p)) \\;\\iff\\; p = \\top. $$$$

Lean4

theorem unique_quotient_iff_eq_top : Nonempty (Unique (M ⧸ p)) ↔ p = ⊤ :=
  ⟨fun ⟨h⟩ => subsingleton_quotient_iff_eq_top.mp (@Unique.instSubsingleton _ h), by rintro rfl;
    exact ⟨QuotientTop.unique⟩⟩

Похожие утверждения