toPGame_nadd — Mathlib

English

Natural addition of ordinals corresponds to addition of their toPGame images, up to equivalence.

Русский

Естественное сложение ординалов соответствует сложению их образов в toPGame, с равенством по эквивалентности.

LaTeX

$$(a ♯ b).toPGame ≈ a.toPGame + b.toPGame$$

Lean4

/-- The natural addition of ordinals corresponds to their sum as games. -/
theorem toPGame_nadd (a b : Ordinal) : (a ♯ b).toPGame ≈ a.toPGame + b.toPGame :=
  by
  refine ⟨le_of_forall_lf (fun i => ?_) isEmptyElim, le_of_forall_lf (fun i => ?_) isEmptyElim⟩
  · rw [toPGame_moveLeft']
    rcases lt_nadd_iff.1 (toLeftMovesToPGame_symm_lt i) with (⟨c, hc, hc'⟩ | ⟨c, hc, hc'⟩) <;>
        rw [← toPGame_le_iff, le_congr_right (toPGame_nadd _ _)] at hc' <;>
      apply lf_of_le_of_lf hc'
    · apply add_lf_add_right
      rwa [toPGame_lf_iff]
    · apply add_lf_add_left
      rwa [toPGame_lf_iff]
  · apply leftMoves_add_cases i <;> intro i <;> let wf := toLeftMovesToPGame_symm_lt i <;>
          (try rw [add_moveLeft_inl]) <;> (try rw [add_moveLeft_inr]) <;>
      rw [toPGame_moveLeft', ← lf_congr_left (toPGame_nadd _ _), toPGame_lf_iff]
    · exact nadd_lt_nadd_right wf _
    · exact nadd_lt_nadd_left wf _
termination_by (a, b)

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