induction — Mathlib

English

Induction principle for Prod.GameAdd given WellFounded rα and rβ.

Русский

Принцип индукции для Prod.GameAdd при заданных WellFounded rα и rβ.

LaTeX

$$$\\text{induction} : (\\text{WellFounded } r_α) \\to (\\text{WellFounded } r_β) \\to (IH) \\to \\forall a,b, C(a,b)$$$

Lean4

/-- Induction on the well-founded `Prod.GameAdd` relation.
  Note that it's strictly more general to induct on the lexicographic order instead. -/
theorem induction {C : α → β → Prop} :
    WellFounded rα →
      WellFounded rβ → (∀ a₁ b₁, (∀ a₂ b₂, GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ a b, C a b :=
  GameAdd.fix

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