English
If, for every S, assuming P(S.erase s) for all s ∈ S implies P(S), then P(S) holds for all S.
Русский
Если для каждого S верно, что P(S.erase s) для всех s ∈ S тогда P(S) для всех S.
LaTeX
$$$\\forall S,\\, (\\forall s \\in S, p(S\\setminus \\{s\\})) \\Rightarrow p(S) \\;\\Rightarrow \\forall S, p(S)$$$
Lean4
/-- To prove a proposition for an arbitrary `Finset α`,
it suffices to prove that for any `S : Finset α`, the following is true:
the property is true for S with any element `s` removed, then the property holds for `S`.
This is a weaker version of `Finset.strongInduction`.
But it can be more precise when the induction argument
only requires removing single elements at a time.
-/
theorem eraseInduction [DecidableEq α] {p : Finset α → Prop} (H : (S : Finset α) → (∀ s ∈ S, p (S.erase s)) → p S)
(S : Finset α) : p S :=
S.strongInduction fun S ih => H S fun _ hs => ih _ (erase_ssubset hs)
