of_neg — Mathlib

English

If -x₁ ≡ -x₂, then x₁ ≡ x₂.

Русский

Если -x₁ эквивалентно -x₂, то x₁ эквивалентно x₂.

LaTeX

$$$$ -x_1 \equiv -x_2 \Rightarrow x_1 \equiv x_2. $$$$

Lean4

/-- If `-x` has the same moves as `-y`, then `x` has the sames moves as `y`. -/
theorem of_neg : ∀ {x₁ x₂ : PGame}, -x₁ ≡ -x₂ → x₁ ≡ x₂
  | mk x₁l x₁r x₁L x₁R, mk x₂l x₂r x₂L x₂R => by
    simpa using Identical.neg (x₁ := mk _ _ (-x₁R ·) (-x₁L ·)) (x₂ := mk _ _ (-x₂R ·) (-x₂L ·))

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