add_left

Mathlib.SetTheory.PGame.Algebra

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

English

If y₁ ≡ y₂, then x + y₁ ≡ x + y₂.

Русский

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

LaTeX

$$$ x + y_1 \equiv x + y_2 $ given\; y_1 \equiv y_2 $$$

Lean4

theorem add_left {x y₁ y₂} (hy : y₁ ≡ y₂) : x + y₁ ≡ x + y₂ :=
  (x.add_comm y₁).trans (hy.add_right.trans (y₂.add_comm x))

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

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

Разделы

Аффилиация

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