English
A set has cardinality 1 if and only if it is a singleton: s.ncard = 1 ⇔ ∃ a, s = {a}.
Русский
Множество имеет кардинальность 1 тогда и только тогда, когда оно является синглтоном: s.ncard = 1 ⇔ ∃ a, s = {a}.
LaTeX
$$$$ s.ncard = 1 \iff \exists a, s = \{a\} $$$$
Lean4
@[simp]
theorem ncard_eq_one : s.ncard = 1 ↔ ∃ a, s = { a } :=
by
refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩
have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h
refine h.imp fun a ha ↦ ?_
simp_rw [Set.ext_iff, mem_singleton_iff]
simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha
exact ha
