equiv_iff_add_equiv_zero

Mathlib.SetTheory.Game.Impartial

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

← MathLib Explorer

English

For impartial G and any H, H ≈ G iff H + G ≈ 0.

Русский

Для непредвзятой G и любого H: H ≈ G ⇔ H + G ≈ 0.

LaTeX

$$$H \approx G \iff H + G \approx 0$$$

Lean4

/-- This lemma doesn't require `H` to be impartial. -/
theorem equiv_iff_add_equiv_zero (H : PGame) : H ≈ G ↔ H + G ≈ 0 := by
  rw [equiv_iff_game_eq, ← add_right_cancel_iff (a := ⟦G⟧), mk'_add_self, ← quot_add, equiv_iff_game_eq, quot_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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