nonempty_quotient_iff — Mathlib

English

Let s be a setoid on α. Then the quotient α/ s is nonempty if and only if α is nonempty.

Русский

Пусть s — множество-эквивалентностей на α. Тогда фактор-множество α/s непусто тогда и только тогда, когда α непусто.

LaTeX

$$$\\operatorname{Nonempty}(\\operatorname{Quotient}(s)) \\iff \\operatorname{Nonempty}(\\alpha)$$$

Lean4

theorem nonempty_quotient_iff (s : Setoid α) : Nonempty (Quotient s) ↔ Nonempty α :=
  ⟨fun ⟨a⟩ ↦ Quotient.inductionOn a Nonempty.intro, fun ⟨a⟩ ↦ ⟨⟦a⟧⟩⟩

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