encard_eq_one — Mathlib

English

encard(s) = 1 if and only if s is a singleton.

Русский

encard(S) = 1 тогда и только тогда S является единичным множеством.

LaTeX

$$$encard(s) = 1 \\iff \\exists x, s = \\{ x \\}$$$

Lean4

theorem encard_eq_one : s.encard = 1 ↔ ∃ x, s = { x } :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩
  obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
  exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le (by simpa) (by simp [h])).symm⟩

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