strongDownwardInduction_eq — Mathlib

English

Equality expressing that strongDownwardInduction(H,s) equals applying H to s with the recursive call to strongDownwardInduction(H,·).

Русский

Равенство, выражающее, что strongDownwardInduction(H,s) равно применению H к s с рекурсивным вызовом к strongDownwardInduction(H,·).

LaTeX

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

Lean4

theorem strongDownwardInduction_eq {p : Multiset α → Sort*} {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) (s : Multiset α) :
    strongDownwardInduction H s = H s fun ht _hst => strongDownwardInduction H _ ht := by rw [strongDownwardInduction]

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