English
A Finset s has cardinality n+1 iff there exists an element a and a finite set t with a ∉ t such that insert a t = s and |t| = n.
Русский
Кардиналитет Finset s равен n+1 тогда и только тогда существует элемент a и множество t с a ∉ t, такое что insert a t = s и |t| = n.
LaTeX
$$$#s = n + 1 \\iff ∃ a \\; ∃ t, a \\notin t ∧ insert a t = s ∧ #t = n$$$
Lean4
theorem card_eq_succ : #s = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ #t = n :=
⟨fun h =>
let ⟨a, has⟩ := card_pos.mp (h.symm ▸ Nat.zero_lt_succ _ : 0 < #s)
⟨a, s.erase a, s.notMem_erase a, insert_erase has, by
simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]⟩,
fun ⟨_, _, hat, s_eq, n_eq⟩ => s_eq ▸ n_eq ▸ card_insert_of_notMem hat⟩
