isOption_neg — Mathlib

English

For all x and y, x has an option to -y if and only if -x has an option to y.

Русский

Для любых x и y имеется опция x к -y тогда и только тогда, когда у -x есть опция к y.

LaTeX

$$$$ \mathrm{IsOption}(x,-y) \iff \mathrm{IsOption}(-x,y). $$$$

Lean4

theorem isOption_neg {x y : PGame} : IsOption x (-y) ↔ IsOption (-x) y :=
  by
  rw [isOption_iff, isOption_iff, or_comm]
  cases y
  apply or_congr <;>
    · apply exists_congr
      intro
      rw [neg_eq_iff_eq_neg]
      simp only [neg_def, moveRight_mk, moveLeft_mk]

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