English
Let a ∉ s. Then for every n, the (n+1)-subsets of insert a s are the union of (n+1)-subsets of s and the image of n-subsets of s with a inserted.
Русский
Пусть a ∉ s. Тогда подмножества размера n+1 of s ∪ {a} состоят из подмножеств без a и подмножеств с добавлением a к подмножествам размера n из s.
LaTeX
$$powersetCard (n+1) (insert a s) = powersetCard (n+1) s ∪ (powersetCard n s).image (insert a)$$
Lean4
theorem powersetCard_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ (powersetCard n s).image (insert x) :=
by
rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
congr
rw [powersetCard_eq_filter, filter_image]
congr 1
ext t
simp only [mem_powerset, mem_filter, and_congr_right_iff]
intro ht
have : x ∉ t := fun H => h (ht H)
simp [card_insert_of_notMem this]
