not_fuzzy_of_le

Mathlib.SetTheory.PGame.Order

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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