le_one_iff_subsingleton — Mathlib

English

The cardinality of α is at most 1 if and only if α is subsingleton.

Русский

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

LaTeX

$$$\\#\\alpha \\le 1 \\;\\Longleftrightarrow\\; \\text{Subsingleton}(\\alpha)$$

Lean4

theorem le_one_iff_subsingleton {α : Type u} : #α ≤ 1 ↔ Subsingleton α :=
  ⟨fun ⟨f⟩ => ⟨fun _ _ => f.injective (Subsingleton.elim _ _)⟩, fun ⟨h⟩ => ⟨fun _ => ULift.up 0, fun _ _ _ => h _ _⟩⟩

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