English
Induction on finite sets: to prove a property motive for a finite set s, it suffices to prove it for the empty set and show that motive t → motive ({a} ∪ t) for all a ∉ t.
Русский
Индукция по конечным множествам: чтобы доказать свойство motive для конечного множества s, достаточно доказать его для пустого множества и показать, что motive t → motive ( {a} ∪ t ) для любого a, не принадлежащего t.
LaTeX
$$$ [elab\\,as\\,elim] \\; \\text{induction_on }(s : Set α)(hs : s.Finite)(empty : motive ∅ finite_empty)(insert : ∀{a s}, a ∉ s → ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) \\, → \\, motive s hs $$$
Lean4
/-- Induction principle for finite sets: To prove a property `motive` of a finite set `s`, it's
enough to prove for the empty set and to prove that `motive t → motive ({a} ∪ t)` for all `t`.
See also `Set.Finite.induction_on` for the version requiring to check `motive t → motive ({a} ∪ t)`
only for `t ⊆ s`. -/
@[elab_as_elim]
theorem induction_on {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ finite_empty)
(insert : ∀ {a s}, a ∉ s → ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) : motive s hs :=
by
lift s to Finset α using id hs
induction s using Finset.cons_induction_on with
| empty => simpa
| cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)
