eq_one_iff_unique — Mathlib

English

The cardinality of a type α is 1 if and only if α is subsingleton and nonempty.

Русский

Кардинал α равен 1 тогда и только тогда, когда α является синглотоном и непустым.

LaTeX

$$$ \#\alpha = 1 \iff \operatorname{Subsingleton} \alpha \wedge \operatorname{Nonempty} \alpha $$$

Lean4

theorem eq_one_iff_unique {α : Type*} : #α = 1 ↔ Subsingleton α ∧ Nonempty α :=
  calc
    #α = 1 ↔ #α ≤ 1 ∧ 1 ≤ #α := le_antisymm_iff
    _ ↔ Subsingleton α ∧ Nonempty α := le_one_iff_subsingleton.and (one_le_iff_ne_zero.trans mk_ne_zero_iff)

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