mulOption_lt_mul_iff_P3 — Mathlib

English

For i ∈ x.LeftMoves and j ∈ y.LeftMoves, the inequality between mulOption and x*y is equivalent to P3 applied to the corresponding moves: mulOption x y i j < (x*y) iff P3(x.moveLeft i) x (y.moveLeft j) y.

Русский

Для i ∈ x.LeftMoves и j ∈ y.LeftMoves неравенство между mulOption и x*y эквивалентно применению P3 к соответствующим ходам: mulOption x y i j < x*y тогда P3(...).

LaTeX

$$$$ (\llbracket mulOption\ x\ y\ i\ j \rrbracket) < (\llbracket x \cdot y \rrbracket) \iff \mathrm{P3}(x.moveLeft i)\ x\ (y.moveLeft j)\ y. $$$$

Lean4

theorem mulOption_lt_mul_iff_P3 {i j} : ⟦mulOption x y i j⟧ < (⟦x * y⟧ : Game) ↔ P3 (x.moveLeft i) x (y.moveLeft j) y :=
  by
  dsimp only [mulOption, quot_sub, quot_add]
  exact sub_lt_iff_lt_add'

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