add_left_inj

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

If IsLeftCancelAdd holds and x ≠ ⊤, then x + y = x + z iff y = z.

Русский

При IsLeftCancelAdd и x ≠ ⊤ имеем x+y = x+z iff y=z.

LaTeX

$$$(IsLeftCancelAdd α) \\; (hx:\\ x \\neq \\top) \\to (x+y = x+z \\iff y = z)$$$

Lean4

theorem add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊤) : x + y = x + z ↔ y = z := by lift x to α using hx;
  cases y <;> cases z <;> simp [← coe_add]

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

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

Разделы

Аффилиация

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