numeric_imp — Mathlib

English

Relabellings preserve being numeric: Numeric x iff Numeric y when x ≡r y.

Русский

Ребаллинги сохраняют числовость: Numeric x эквивалентно Numeric y при x ≡r y.

LaTeX

$$$(\text{Relabelling } x \ y) \Rightarrow (\text{Numeric } x \leftrightarrow \text{Numeric } y)$$$

Lean4

theorem numeric_imp {x y : PGame} (r : x ≡r y) (ox : Numeric x) : Numeric y :=
  by
  induction x using PGame.moveRecOn generalizing y with
  | _ x IHl IHr
  apply Numeric.mk (fun i j => ?_) (fun i => ?_) fun j => ?_
  · rw [← lt_congr (r.moveLeftSymm i).equiv (r.moveRightSymm j).equiv]
    apply ox.left_lt_right
  · exact IHl _ (r.moveLeftSymm i) (ox.moveLeft _)
  · exact IHr _ (r.moveRightSymm j) (ox.moveRight _)

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