lt_or_equiv_or_gf

Mathlib.SetTheory.PGame.Order

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

← MathLib Explorer

English

Alternatively, x < y, or x ≈ y, or y ⧏ x holds.

Русский

Иначе выполняется одно из: x < y, или x ≈ y, или y ⧏ x.

LaTeX

$$$x < y \lor (x \approx y) \lor y \vartriangleleft x$$$

Lean4

theorem lt_or_equiv_or_gf (x y : PGame) : x < y ∨ (x ≈ y) ∨ y ⧏ x :=
  by
  rw [lf_iff_lt_or_fuzzy, Fuzzy.swap_iff]
  exact lt_or_equiv_or_gt_or_fuzzy x y

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

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

Разделы

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

Аффилиация

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