not_equiv

Mathlib.SetTheory.PGame.Order

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

English

If x ≈ y, then x and y are not fuzzy with each other.

Русский

Если x эквивалентно y, то x и y не неразборчивы между собой.

LaTeX

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

Lean4

theorem not_equiv {x y : PGame} (h : x ‖ y) : ¬(x ≈ y) := fun h' => h'.1.not_gf h.2

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

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

Разделы

Аффилиация

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