add — Mathlib

English

The sum of two numeric games is numeric.

Русский

Сумма двух числовых игр числова.

LaTeX

$$$(\forall x,y, Numeric(x) \land Numeric(y)) \Rightarrow Numeric(x+y)$$$

Lean4

theorem add : ∀ {x y : PGame} (_ : Numeric x) (_ : Numeric y), Numeric (x + y)
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩, ox, oy =>
    ⟨by
      rintro (ix | iy) (jx | jy)
      · exact add_lt_add_right (ox.1 ix jx) _
      ·
        exact
          (add_lf_add_of_lf_of_le (lf_mk _ _ ix) (oy.le_moveRight jy)).lt ((ox.moveLeft ix).add oy)
            (ox.add (oy.moveRight jy))
      ·
        exact
          (add_lf_add_of_lf_of_le (mk_lf _ _ jx) (oy.moveLeft_le iy)).lt (ox.add (oy.moveLeft iy))
            ((ox.moveRight jx).add oy)
      · exact add_lt_add_left (oy.1 iy jy) ⟨xl, xr, xL, xR⟩,
      by
      constructor
      · rintro (ix | iy)
        · exact (ox.moveLeft ix).add oy
        · exact ox.add (oy.moveLeft iy)
      · rintro (jx | jy)
        · apply (ox.moveRight jx).add oy
        · apply ox.add (oy.moveRight jy)⟩
termination_by x y =>
  (x, y) -- Porting note: Added `termination_by`

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