strongInductionOn_eq — Mathlib

English

Equality between strongInductionOn s and the explicit expression holds.

Русский

Справедливость равенства между strongInductionOn s и явным выражением.

LaTeX

$$$\\text{strongInductionOn}(s, H) = H\\,s(\\lambda t, \\_ => t.strongInductionOn(H))$$$

Lean4

theorem strongInductionOn_eq {p : Finset α → Sort*} (s : Finset α) (H : ∀ s, (∀ t ⊂ s, p t) → p s) :
    s.strongInductionOn H = H s fun t _ => t.strongInductionOn H :=
  by
  dsimp only [strongInductionOn]
  rw [strongInduction]

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