neg_equiv_neg_iff — Mathlib

English

Let x and y be P-games. Then -x is equivalent to -y if and only if x is equivalent to y.

Русский

Пусть x и y — P-игры. Тогда -x эквивалентно -y тогда и только тогда, когда x эквивалентно y.

LaTeX

$$$-x \\approx -y \\iff x \\approx y$$$

Lean4

@[simp]
theorem neg_equiv_neg_iff {x y : PGame} : -x ≈ -y ↔ x ≈ y :=
  by
  change Equiv (-x) (-y) ↔ Equiv x y
  rw [Equiv, Equiv, neg_le_neg_iff, neg_le_neg_iff, and_comm]

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