congr_right — Mathlib

English

If x ≡ y, then for all w, w ∈ᵣ x iff w ∈ᵣ y.

Русский

Если x идентичен y, то для любого w верно: w принадлежит x справа тогда и только тогда, когда w принадлежит y справа.

LaTeX

$$$ \forall {x y : PGame}, x \equiv y \\rightarrow (\forall {w : PGame}, w \in_\mathrm{r} x \leftrightarrow w \in_\mathrm{r} y)$$$

Lean4

theorem congr_right : ∀ {x y : PGame}, x ≡ y → (∀ {w : PGame}, w ∈ᵣ x ↔ w ∈ᵣ y)
  | mk _ _ _ _, mk _ _ _ _, ⟨_, ⟨h₁, h₂⟩⟩, _w =>
    ⟨fun ⟨i, hi⟩ ↦ (h₁ i).imp (fun _ ↦ hi.trans), fun ⟨j, hj⟩ ↦ (h₂ j).imp (fun _ hi ↦ hj.trans hi.symm)⟩

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