English
A variant of induction on Finset: from empty and a step rule with a ∈ s, deduce the property for all s.
Русский
Вариант индукции по Finset: из пустого по правилу шага с a ∈ s выводим свойство для всех s.
LaTeX
$$$\\text{induction_on}(s, empty, insert) \\Rightarrow \\text{motive}(s)$$$
Lean4
/-- To prove a proposition about an arbitrary `Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α`,
then it holds for the `Finset` obtained by inserting a new element.
-/
@[elab_as_elim]
protected theorem induction_on {α : Type*} {motive : Finset α → Prop} [DecidableEq α] (s : Finset α) (empty : motive ∅)
(insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : motive s :=
Finset.induction empty insert s
