lt_or_fuzzy_of_lf

Mathlib.SetTheory.PGame.Order

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

English

If x LF y, then either x < y or x is fuzzy with y.

Русский

Если x LF y, то либо x < y, либо x неразборчиво с y.

LaTeX

$$$x \vartriangleleft y \Rightarrow x < y \lor x \|\| y$$$

Lean4

theorem lt_or_fuzzy_of_lf {x y : PGame} : x ⧏ y → x < y ∨ x ‖ y :=
  lf_iff_lt_or_fuzzy.1

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

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

Разделы

Аффилиация

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