card_le_one_iff_subsingleton — Mathlib

English

For a finite α, Nat.card α ≤ 1 if and only if α is a subsingleton.

Русский

Для конечного α: Nat.card α ≤ 1 тогда и только тогда, когда α является подподмножеством по одному элементу (субоднородным).

LaTeX

$$$Nat.card(\alpha) ≤ 1 \iff Subsingleton(\alpha)$$$

Lean4

theorem card_le_one_iff_subsingleton [Finite α] : Nat.card α ≤ 1 ↔ Subsingleton α :=
  by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]

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