isOrderedAddMonoid — Mathlib

English

PartENat, equipped with addition, forms an IsOrderedAddMonoid; in particular, addition preserves order: if a ≤ b, then a + c ≤ b + c for all c.

Русский

PartENat вместе с сложением образует упорядоченную аддитивную моноиду; в частности, сложение сохраняет порядок: если a ≤ b, то a + c ≤ b + c для любого c.

LaTeX

$$$ \text{IsOrderedAddMonoid}(\mathrm{PartENat}) $$$

Lean4

noncomputable instance isOrderedAddMonoid : IsOrderedAddMonoid PartENat :=
  {
    add_le_add_left := fun a b ⟨h₁, h₂⟩ c =>
      PartENat.casesOn c (by simp [top_add]) fun c =>
        ⟨fun h => And.intro (dom_natCast _) (h₁ h.2), fun h => by
          simpa only [coe_add_get] using add_le_add_left (h₂ _) c⟩ }

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