neg_identical_neg

Mathlib.SetTheory.PGame.Algebra

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

English

For all x,y: -x ≡ -y ↔ x ≡ y.

Русский

Для любых x,y: -x эквивалентно -y ↔ x эквивалентно y.

LaTeX

$$$$ -x \equiv -y \iff x \equiv y. $$$$

Lean4

@[simp]
theorem neg_identical_neg {x y : PGame} : -x ≡ -y ↔ x ≡ y :=
  ⟨Identical.of_neg, Identical.neg⟩

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

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

Разделы

Аффилиация

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