strongInductionOn_eq — Mathlib

English

The evaluation of strong downward induction on s is equal to applying the rule to s and recursing on t.

Русский

Значение сильного нисходящего индуктивного образования по s равно применению правила к s и рекурсии по t.

LaTeX

$$$\\text{strongDownwardInduction}(H,s) = H\\left(s,\\lambda t\\; ht\\;\\_,\\ \\text{strongDownwardInduction}(H,t)\\right)$$$

Lean4

theorem strongInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) (H) :
    @strongInductionOn _ p s H = H s fun t _h => @strongInductionOn _ p t H := by rw [strongInductionOn]

Похожие утверждения