subsingleton_of_not_nonempty — Mathlib

English

If α is not nonempty (i.e., empty), then α is a subsingleton (any two elements are equal).

Русский

Если α пустой, тогда α — сингельтон (любые две элементы равны).

LaTeX

$$$\forall {\alpha : \text{Sort*}}, \neg \mathrm{Nonempty}(\alpha) \Rightarrow \mathrm{Subsingleton}(\alpha)$$$

Lean4

theorem subsingleton_of_not_nonempty {α : Sort*} (h : ¬Nonempty α) : Subsingleton α :=
  ⟨fun x ↦ False.elim <| not_nonempty_iff_imp_false.mp h x⟩

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