sym2_gameAdd — Mathlib

English

If rα is well-founded, then Sym2.GameAdd rα is well-founded.

Русский

Если rα хорошо установлен (well-founded), то Sym2.GameAdd rα также хорошо установлен.

LaTeX

$$$\text{WellFounded}(r_\alpha) \Rightarrow \text{WellFounded}(\mathrm{Sym2.GameAdd}(r_\alpha)).$$$

Lean4

/-- The `Sym2.GameAdd` relation on well-founded inputs is well-founded. -/
theorem sym2_gameAdd (h : WellFounded rα) : WellFounded (Sym2.GameAdd rα) :=
  ⟨fun i => Sym2.inductionOn i fun x y => (h.apply x).sym2_gameAdd (h.apply y)⟩

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