card_eq_one_iff_unique — Mathlib

English

card α = 1 if and only if α has a unique element (i.e., a singleton up to isomorphism).

Русский

card α = 1 тогда и только тогда, когда α имеет уникальный элемент (одноэлементный множество).

LaTeX

$$$\operatorname{card}(\alpha) = 1 \;\iff\; \text{Nonempty}(\alpha) \land \text{Unique}(\alpha)$$$

Lean4

theorem card_eq_one_iff_unique {α : Type*} : card α = 1 ↔ Nonempty (Unique α) :=
  by
  rw [unique_iff_subsingleton_and_nonempty α, le_antisymm_iff]
  exact and_congr (card_le_one_iff_subsingleton α) (one_le_card_iff_nonempty α)

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