not_equiv'

Mathlib.SetTheory.PGame.Order

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

English

If x ≈ y, then y is not equivalent to x.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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