strongInduction_eq — Mathlib

English

Equality between the strongInduction H s and H s applied to the result of strongInduction on smaller sets holds.

Русский

Эквивалентность между strongInduction H s и H s, примененным к результату strongInduction на меньших множествах.

LaTeX

$$$\\text{strongInduction}(H)\\,s = H\\,s\\bigl(\\lambda t,\\_;\\text{strongInduction}(H)\\,t\\bigr)$$$

Lean4

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

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