English
A standard induction principle: P(∅) and P(s) ⇒ P(insert a s) imply P(s) for all Finset s.
Русский
Стандартная индукция по Finset: P(∅) и P(s) ⇒ P(insert a s) для любого a дают P(s) для всех s.
LaTeX
$$$P(\\emptyset) \\land \\forall a\\,s (a \\notin s)\\; P(s) \\Rightarrow P(\\operatorname{insert}(a,s)) \\Rightarrow \\forall s\\ P(s)$$$
Lean4
@[elab_as_elim]
protected theorem induction {α : Type*} {motive : Finset α → Prop} [DecidableEq α] (empty : motive ∅)
(insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : ∀ s, motive s :=
cons_induction empty fun a s ha => (s.cons_eq_insert a ha).symm ▸ insert a s ha
