English
To prove a proposition about Finset α, it suffices to prove it for all singletons and that if it holds for s, then it holds for Finset.cons a s h.
Русский
Чтобы доказать свойство про Finset α, достаточно доказать его для всех одиночных множеств и показать, что если оно действует для s, то и для Finset.cons a s h.
LaTeX
$$$\\forall a,s\\; (h: a \\notin s), P(s) \\Rightarrow P(\\operatorname{cons}(a,s,h))$ и базовый случай $P(\\emptyset)$ дают $\\forall s\\ P(s)$$$
Lean4
@[elab_as_elim]
theorem cons_induction {α : Type*} {motive : Finset α → Prop} (empty : motive ∅)
(cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : ∀ s, motive s
| ⟨s, nd⟩ => by
induction s using Multiset.induction with
| empty => exact empty
| cons a s IH =>
rw [mk_cons nd]
exact cons a _ _ (IH _)
