not_equiv_zero_iff

Mathlib.SetTheory.Game.Impartial

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

English

Not equivalent to 0 iff G is fuzzy with 0.

Русский

Не эквивалентно 0 тогда и только тогда, когда G неразрешима с 0.

LaTeX

$$$\neg(G \approx 0) \iff G \parallel 0$$$

Lean4

@[simp]
theorem not_equiv_zero_iff : ¬G ≈ 0 ↔ G ‖ 0 :=
  ⟨(equiv_or_fuzzy_zero G).resolve_left, Fuzzy.not_equiv⟩

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

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

Разделы

Аффилиация

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