strongDownwardInductionOn_eq — Mathlib

English

Equality for the swapped-argument form of the downward strong induction principle.

Русский

Равенство для формы нисходящей сильной индукции с изменённым порядком аргументов.

LaTeX

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

Lean4

theorem strongDownwardInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) :
    s.strongDownwardInductionOn H = H s fun {t} ht _h => t.strongDownwardInductionOn H ht :=
  by
  dsimp only [strongDownwardInductionOn]
  rw [strongDownwardInduction]

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