strongDownwardInductionOn_eq — Mathlib

English

Equality between strongDownwardInductionOn s and the corresponding H-form holds.

Русский

Справедливость равенства между strongDownwardInductionOn и соответствующим H-образованием.

LaTeX

$$$\\text{strongDownwardInductionOn}(s) = H\\,s(\\lambda t, h => \\text{strongDownwardInductionOn}(t))$$$

Lean4

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

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