not_fuzzy

Mathlib.SetTheory.PGame.Order

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

English

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

Русский

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

LaTeX

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

Lean4

theorem not_fuzzy {x y : PGame} (h : x ≈ y) : ¬x ‖ y :=
  not_fuzzy_of_le h.1

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

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

Разделы

Аффилиация

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