instTransEquivLt

Mathlib.SetTheory.PGame.Order

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

← MathLib Explorer

English

If x1 ≈ x2, 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

instance : Trans ((· ≈ ·) : PGame → PGame → Prop) ((· < ·) : PGame → PGame → Prop) ((· < ·) : PGame → PGame → Prop)
    where trans := lt_of_equiv_of_lt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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