addLeftReflectLT — Mathlib

English

WithBot α supports a left-reflect LT: if a < b then a + c < b + c for all c.

Русский

WithBot α поддерживает лево-отражённое отношение LT: если a < b, то a + c < b + c для всех c.

LaTeX

$$$ \\text{instance } AddLeftReflectLT (\\mathrm{WithBot}\\,\\alpha)$$$

Lean4

instance addLeftReflectLT [LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithBot α) where
  elim x y z := by cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using lt_of_add_lt_add_left

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