card_eq_one_iff_unique — Mathlib

English

Nat.card α = 1 if and only if there exists x ∈ α with ∀ y ∈ α, y = x.

Русский

Nat.card α = 1 тогда и только тогда, когда существует x ∈ α такой, что для всех y ∈ α верно y = x.

LaTeX

$$$$ Nat.card(\alpha) = 1 \iff (\exists x \in \alpha, \forall y \in \alpha, y = x) $$$$

Lean4

theorem card_eq_one_iff_unique : Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α :=
  Cardinal.toNat_eq_one_iff_unique

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