instIsOrderedAddMonoid — Mathlib

English

If Y is a lattice-ordered additive group, then LocallyFinsuppWithin(U,Y) forms an ordered additive monoid compatible with the lattice structure.

Русский

Если Y является упорядоченной аддитивной группой, LocallyFinsuppWithin(U,Y) образует упорядоченную аддитивную моноиду совместно с граниченной решёткой.

LaTeX

$$$\\text{IsOrderedAddMonoid}(\\text{LocallyFinsuppWithin}(U,Y))$$$

Lean4

/-- Functions with locally finite support within `U` form an ordered commutative group.
-/
instance [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] : IsOrderedAddMonoid (locallyFinsuppWithin U Y) where
  add_le_add_left := fun _ _ _ _ ↦ by simpa [le_def]

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