add_left_inj

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

If x ≠ ⊥ and x + y = x + z, then y = z (left-injectivity).

Русский

Если x ≠ ⊥ и x + y = x + z, то y = z (левая инъекция).

LaTeX

$$$ [IsLeftCancelAdd \\alpha] (hx : x \\neq \\bot) : 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