prod_gameAdd — Mathlib

English

If rα and rβ are well-founded, then Prod.GameAdd rα rβ is well-founded.

Русский

Если rα и rβ хорошо основаны, то Prod.GameAdd rα rβ хорошо основано.

LaTeX

$$$\\text{WellFounded } r_α \\rightarrow \\text{WellFounded } r_β \\rightarrow \\text{WellFounded } (Prod.GameAdd r_α r_β)$$$

Lean4

/-- The `Prod.GameAdd` relation on well-founded inputs is well-founded.

  In particular, the sum of two well-founded games is well-founded. -/
theorem prod_gameAdd (hα : WellFounded rα) (hβ : WellFounded rβ) : WellFounded (Prod.GameAdd rα rβ) :=
  ⟨fun ⟨a, b⟩ => (hα.apply a).prod_gameAdd (hβ.apply b)⟩

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