not_fuzzy'

Mathlib.SetTheory.PGame.Order

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

English

If x ≈ y, then not y ‖ x.

Русский

Если x эквивалентно y, то не y ‖ x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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