strongInductionOn — Mathlib

English

An analogue of strong induction where the order of the arguments is swapped.

Русский

Аналог сильной индукции, где порядок аргументов поменян.

LaTeX

$$$\\text{strongInductionOn} \\, {p} \\, (s) = s.\\text{strongInductionOn} (H)$$$

Lean4

/-- Analogue of `strongInduction` with order of arguments swapped. -/
@[elab_as_elim]
def strongInductionOn {p : Finset α → Sort*} (s : Finset α) : (∀ s, (∀ t ⊂ s, p t) → p s) → p s := fun H =>
  strongInduction H s

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