addLeftReflectLE — Mathlib

English

Let M be an additive monoid with a preorder and AddLeftStrictMono. Then the positive subset { x in M | 0 < x } inherits left-translation LE: if a ≤ b with a,b > 0, then a + c ≤ b + c for all c > 0.

Русский

Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов наследует левое отражение LE: если a ≤ b и a,b > 0, то a + c ≤ b + c для всех c > 0.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, a \\\\le b \\\\Rightarrow a + c \\\\le b + c.$$$

Lean4

instance addLeftReflectLE [AddLeftReflectLE M] : AddLeftReflectLE { x : M // 0 < x } :=
  ⟨fun _ _ _ h => Subtype.coe_le_coe.1 <| le_of_add_le_add_left h⟩

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