le_congr_imp

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.le_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 \le y_1\Rightarrow x_2 \le y_2$$$

Lean4

theorem le_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ ≤ y₁) : x₂ ≤ y₂ :=
  hx.2.trans (h.trans hy.1)

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

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

Разделы

Аффилиация

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