neg — Mathlib

English

If -x₁ and -x₂ have the same moves, then x₁ and x₂ have the same moves.

Русский

Если -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 neg : ∀ {x₁ x₂ : PGame}, x₁ ≡ x₂ → -x₁ ≡ -x₂
  | mk _ _ _ _, mk _ _ _ _, ⟨⟨hL₁, hL₂⟩, ⟨hR₁, hR₂⟩⟩ =>
    ⟨⟨fun i ↦ (hR₁ i).imp (fun _ ↦ Identical.neg), fun j ↦ (hR₂ j).imp (fun _ ↦ Identical.neg)⟩,
      ⟨fun i ↦ (hL₁ i).imp (fun _ ↦ Identical.neg), fun j ↦ (hL₂ j).imp (fun _ ↦ Identical.neg)⟩⟩

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