mulOption_lt_iff_P1 — Mathlib

English

The left-option comparison between mulOption terms corresponds exactly to a P1 condition on the corresponding moves.

Русский

Сравнение левых вариантов mulOption точно соответствует условию P1 на соответствующие ходы.

LaTeX

$$$\\forall {x_1 x_2 y} \\ hx \\ IH24 x_1 x_2 y \\to (\\forall i \\in x_1.LeftMoves)(\\forall k \\in y.LeftMoves), \\,(\\mathrm{lt}(Quotient.mk s (x_1.mulOption y i k)) (Quotient.mk s (instHMul.hMul x_2 y)))$$

Lean4

theorem mulOption_lt_iff_P1 {i j k l} :
    (⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧ ↔
      P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l) :=
  by
  dsimp only [P1, mulOption, quot_sub, quot_add]
  simp_rw [neg_sub', neg_add, quot_mul_neg, neg_neg]

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