lt_or_equiv_of_le

Mathlib.SetTheory.PGame.Order

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

English

If x ≤ y, then either x < y or x ≈ y.

Русский

Если x ≤ y, то либо x < y, либо x ≈ y.

LaTeX

$$$\forall x,y \in \mathrm{PGame},\ x \le y\Rightarrow (x < y) \lor (x \approx y)$$$

Lean4

theorem lt_or_equiv_of_le {x y : PGame} (h : x ≤ y) : x < y ∨ (x ≈ y) :=
  and_or_left.mp ⟨h, (em <| y ≤ x).symm.imp_left PGame.not_le.1⟩

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

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

Разделы

Аффилиация

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