English
If p holds for the empty set, and if p holds for insertions from any a into s provided p holds for all subsets, then p holds for all Finsets.
Русский
Если для пустого множества выполняется p, и если из любого a можно получить p (при условии, что p выполняется для всех подмножеств), то p выполняется для всех Finset.
LaTeX
$$$\\text{case_strong_induction_on} \\, (s : Finset α) \\, (h_0 : p(\\emptyset)) \\, (h_1 : \\forall a\\ s, a \\notin s \\to (\\forall t \\subseteq s, p(t)) \\to p(\\operatorname{insert} a\, s)) : p(s)$$$
Lean4
@[elab_as_elim]
theorem case_strong_induction_on [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h₀ : p ∅)
(h₁ : ∀ a s, a ∉ s → (∀ t ⊆ s, p t) → p (insert a s)) : p s :=
Finset.strongInductionOn s fun s =>
Finset.induction_on s (fun _ => h₀) fun a s n _ ih =>
(h₁ a s n) fun t ss => ih _ (lt_of_le_of_lt ss (ssubset_insert n) : t < _)
