strongDownwardInductionOn — Mathlib

English

Equality relating the swapped-argument version of the downward induction to the standard one.

Русский

Равенство между версией нисходящей индукции с пересмененными аргументами и стандартной версией.

LaTeX

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

Lean4

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

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