English
A Finset s has cardinality n+1 iff there exist an element a and a Finset t with a not in t such that s = cons a t and |t| = n.
Русский
Кардиналитет Finset s равен n+1 тогда и только тогда, существует элемент a и подмножество t с a не принадлежит t, такое что s = cons a t и |t| = n.
LaTeX
$$$#s = n + 1 \\iff \\exists a t, a \\notin t ∧ cons a t a = s ∧ #t = n$$$
Lean4
theorem card_eq_succ_iff_cons : #s = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n :=
⟨cons_induction_on s (by simp) fun a s _ _ _ => ⟨a, s, by simp_all⟩, fun ⟨a, t, _, hs, _⟩ => by simpa [← hs]⟩