lt_congr_right

Mathlib.SetTheory.PGame.Order

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

English

If y1 ≈ y2, then x < y1 ↔ x < y2.

Русский

Если y1 ≈ y2, тогда x < y1 ↔ x < y2.

LaTeX

$$$\forall x,y_1,y_2 \in \mathrm{PGame},\ y_1 \approx y_2\Rightarrow (x < y_1 \leftrightarrow x < y_2)$$$

Lean4

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

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

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

Разделы

Аффилиация

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