equiv_congr_right — Mathlib

English

If x1 ≈ x2, then for all y1, x1 ≈ y1 ↔ x2 ≈ y1.

Русский

Если x1 ≈ x2, тогда для всех y1: x1 ≈ y1 ↔ x2 ≈ y1.

LaTeX

$$$\forall x_1,x_2:\mathrm{PGame},\ (x_1 \approx x_2) \rightarrow \forall y_1:\mathrm{PGame},\ (x_1 \approx y_1) \leftrightarrow (x_2 \approx y_1)$$$

Lean4

theorem equiv_congr_right {x₁ x₂ : PGame} : (x₁ ≈ x₂) ↔ ∀ y₁, (x₁ ≈ y₁) ↔ (x₂ ≈ y₁) :=
  ⟨fun h _ => ⟨fun h' => Equiv.trans (Equiv.symm h) h', fun h' => Equiv.trans h h'⟩, fun h => (h x₂).2 <| equiv_rfl⟩

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