lf_iff_lt_or_fuzzy

Mathlib.SetTheory.PGame.Order

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

English

Left-fore order LF satisfies x ⧏ y if and only if x < y or x is fuzzy with y.

Русский

Упорядочение LF удовлетворяет x ⧏ y тогда и только тогда, когда x < y или x и y неразборчивы.

LaTeX

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

Lean4

theorem lf_iff_lt_or_fuzzy {x y : PGame} : x ⧏ y ↔ x < y ∨ x ‖ y :=
  by
  simp only [lt_iff_le_and_lf, Fuzzy, ← PGame.not_le]
  tauto

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

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

Разделы

Аффилиация

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