strongDownwardInduction_eq — Mathlib

English

Equality between the downward induction operator and its explicit recursive form holds.

Русский

Справедливость равенства между downward-индукцией и её явной рекурсивной формой.

LaTeX

$$$\\text{strongDownwardInduction}(H\\,)(s) = H\\,s(\\lambda t, h \\Rightarrow \\text{strongDownwardInduction}(H)(t))$$$

Lean4

theorem strongDownwardInduction_eq {p : Finset α → Sort*}
    (H : ∀ t₁, (∀ {t₂ : Finset α}, #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁) (s : Finset α) :
    strongDownwardInduction H s = H s fun {t} ht _ => strongDownwardInduction H t ht := by rw [strongDownwardInduction]

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