equiv_zero_iff_ge

Mathlib.SetTheory.Game.Impartial

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

English

Let G be an impartial game. Then G is equivalent to 0 if and only if 0 is less than or equal to G, i.e., 0 ≤ G ⇔ G ≈ 0.

Русский

Пусть G — непредвзятая игра. Тогда 0 ≤ G эквивалентно G ≈ 0.

LaTeX

$$$ [\text{Impartial}(G)] \rightarrow \bigl( G \approx 0 \iff 0 \le G \bigr) $$$

Lean4

theorem equiv_zero_iff_ge : (G ≈ 0) ↔ 0 ≤ G :=
  ⟨And.right, fun h => ⟨le_zero_iff.2 h, h⟩⟩

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

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

Разделы

Аффилиация

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