le_congr_left

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.le_congr_left

English

If x1 ≈ x2, then x1 ≤ y ⇔ x2 ≤ y for any y.

Русский

Если x1 ≈ x2, то для любого y выполняется x1 ≤ y ⇔ x2 ≤ y.

LaTeX

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

Lean4

theorem le_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁ ≤ y ↔ x₂ ≤ y :=
  le_congr hx equiv_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru