English
The strong downward induction principle can be expressed as an equality: the evaluation of strong induction on s equals applying the defining rule to s with the recursive call inside.
Русский
Сильное нисходящее индукционное образование равняется применению правила к s с рекурсивным вызовом внутри.
LaTeX
$$$\\operatorname{strongInductionOn}(p)(s) = (\\text{ih}\\; s)\\bigl(\\lambda t\\;\\_h,\\ \\operatorname{strongInductionOn}(p)(t)\\bigr)$$$
Lean4
/-- The strong induction principle for multisets. -/
@[elab_as_elim]
def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s, (∀ t < s, p t) → p s) : p s :=
(ih s) fun t _h => strongInductionOn t ih
termination_by card s
decreasing_by exact card_lt_card _h
