add_le_add_iff_left — Mathlib

English

For α with LE, AddLeftMono α, and AddLeftReflectLE α, and x ≠ ⊥, we have x + y ≤ x + z iff y ≤ z.

Русский

Для α со свойством LE, AddLeftMono α и AddLeftReflectLE α, и x ≠ ⊥, выполнено x + y ≤ x + z экв. y ≤ z.

LaTeX

$$$$\\forall x,y,z \\in \\mathrm{WithBot}(\\alpha),\\ x \\neq \\bot \\;\\Rightarrow\\; (x+y \\le x+z) \\Leftrightarrow (y \\le z).$$$$

Lean4

protected theorem add_le_add_iff_left [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
    x + y ≤ x + z ↔ y ≤ z :=
  ⟨WithBot.le_of_add_le_add_left hx, (add_le_add_left · _)⟩

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