card_eq_one_iff — Mathlib

English

Let α be a finite type. Then card α = 1 if and only if there exists an element x in α such that every y in α equals x.

Русский

Пусть α — конечный тип. Тогда кардинал α равен 1 тогда и только тогда, когда существует элемент x ∈ α такой, что каждый y ∈ α равен x.

LaTeX

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

Lean4

theorem card_eq_one_iff : card α = 1 ↔ ∃ x : α, ∀ y, y = x :=
  by
  rw [← card_unit, card_eq]
  exact
    ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩, fun ⟨x, hx⟩ =>
      ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ => Subsingleton.elim _ _⟩⟩⟩

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