le_congr — Mathlib

English

If x1 ≈ x2 and y1 ≈ y2, then x1 ≤ y1 if and only if x2 ≤ y2.

Русский

Если x1 ≈ x2 и y1 ≈ y2, тогда x1 ≤ y1 тогда и только тогда x2 ≤ y2.

LaTeX

$$$\forall x_1,y_1,x_2,y_2 \in \mathrm{PGame},\ x_1 \approx x_2\land y_1 \approx y_2\Rightarrow (x_1 \le y_1 \leftrightarrow x_2 \le y_2)$$$

Lean4

theorem le_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ ≤ y₁ ↔ x₂ ≤ y₂ :=
  ⟨le_congr_imp hx hy, le_congr_imp (Equiv.symm hx) (Equiv.symm hy)⟩

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