lt_congr_left

Mathlib.SetTheory.PGame.Order

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

English

If x1 ≈ x2, then x1 < y ↔ x2 < y for any y.

Русский

Если x1 ≈ x2, тогда x1 < y ↔ x2 < y для любого y.

LaTeX

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

Lean4

theorem lt_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁ < y ↔ x₂ < y :=
  lt_congr hx equiv_rfl

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

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

Разделы

Аффилиация

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