lt_congr_imp

Mathlib.SetTheory.PGame.Order

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

English

If x1 ≈ x2 and y1 ≈ y2 and x1 < y1, then 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\land x_1 < y_1\Rightarrow x_2 < y_2$$$

Lean4

theorem lt_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ < y₁) : x₂ < y₂ :=
  hx.2.trans_lt (h.trans_le hy.1)

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

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

Разделы

Аффилиация

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