not_fuzzy_of_ge

Mathlib.SetTheory.PGame.Order

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

English

If y ≤ x, then x is not fuzzy with y.

Русский

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

LaTeX

$$$y \le x \Rightarrow \neg (x \|\| y)$$$

Lean4

theorem not_fuzzy_of_ge {x y : PGame} (h : y ≤ x) : ¬x ‖ y := fun h' => h'.1.not_ge h

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

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

Разделы

Аффилиация

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