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_\ell x \leftrightarrow w \in_\ell 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)⟩

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