toIsOrderedAddMonoid — Mathlib

English

Let α be an IdemSemiring. Then its additive structure is an ordered additive monoid, i.e. addition is monotone in the left argument: for all a ≤ b and all c, a + c ≤ b + c.

Русский

Пусть α — IdemSemiring. Тогда его аддитивная структура образует упорядоченную аддитивную моноиду: сумма сохраняет порядок слева, то есть для всяких a ≤ b и любого c выполняется a + c ≤ b + c.

LaTeX

$$$\forall a,b,c \in \alpha,\ a \le b \Rightarrow a + c \le b + c$$$

Lean4

instance (priority := 100) toIsOrderedAddMonoid : IsOrderedAddMonoid α :=
  {
    add_le_add_left := fun a b hbc c ↦ by
      simp_rw [add_eq_sup]
      grw [hbc] }
    -- See note [lower instance priority]

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