add_right_cancel

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.add_right_cancel

English

If IsRightCancelAdd holds and hz : z ≠ ⊤, then from x + z = y + z one can deduce x = y.

Русский

Если IsRightCancelAdd и hz: z ≠ ⊤, то из x+z = y+z следует x = y.

LaTeX

$$$(IsRightCancelAdd α)\\; (hz:\\ z \\neq \\top) \\to (x+z = y+z \\Rightarrow x = y)$$$

Lean4

theorem add_right_cancel [IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) : x = y :=
  (WithTop.add_right_inj hz).1 h

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

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

Разделы

Аффилиация

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