English
A strengthened induction principle on Finset S: prove for ∅ and extend by inserting a ∈ S with appropriate subset condition.
Русский
Усиленная индукция по Finset S: доказать для ∅ и перейти к insert a s при a ∈ S и подмножество.
LaTeX
$$$\\text{induction_on}'(S, empty, insert) \\Rightarrow \\text{motive}(S)$$$
Lean4
/-- To prove a proposition about `S : Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α ⊆ S`,
then it holds for the `Finset` obtained by inserting a new element of `S`.
-/
@[elab_as_elim]
theorem induction_on' {α : Type*} {motive : Finset α → Prop} [DecidableEq α] (S : Finset α) (empty : motive ∅)
(insert : ∀ (a s), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (insert a s)) : motive S :=
@Finset.induction_on α (fun T => T ⊆ S → motive T) _ S (fun _ => empty)
(fun a s has hqs hs =>
let ⟨hS, sS⟩ := Finset.insert_subset_iff.1 hs
insert a s hS sS has (hqs sS))
(Finset.Subset.refl S)
