card_eq_one_iff_nonempty_unique — Mathlib

English

The finite type α has cardinality 1 if and only if α has a unique element, i.e., there exists x ∈ α such that for all y ∈ α, y = x.

Русский

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

LaTeX

$$$\\operatorname{card} \\alpha = 1 \\iff \\exists x: \\alpha, \\forall y: \\alpha, y = x$$$

Lean4

theorem card_eq_one_iff_nonempty_unique : card α = 1 ↔ Nonempty (Unique α) :=
  ⟨fun h =>
    let ⟨d, h⟩ := Fintype.card_eq_one_iff.mp h
    ⟨{  default := d
        uniq := h }⟩,
    fun ⟨_h⟩ => Fintype.card_unique⟩

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