strongDownwardInductionOn — Mathlib

English

An analogue of strongDownwardInduction with the order of arguments swapped.

Русский

Аналог сильной нисходящей индукции с изменённым порядком аргументов.

LaTeX

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

Lean4

/-- Analogue of `strongDownwardInduction` with order of arguments swapped. -/
@[elab_as_elim]
def strongDownwardInductionOn {p : Finset α → Sort*} (s : Finset α)
    (H : ∀ t₁, (∀ {t₂ : Finset α}, #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁) : #s ≤ n → p s :=
  strongDownwardInduction H s

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