isOrderedAddMonoid — Mathlib

English

WithBot α is an IsOrderedAddMonoid provided α has AddCommMonoid, PartialOrder, and IsOrderedAddMonoid.

Русский

WithBot α является IsOrderedAddMonoid при наличии у α AddCommMonoid, PartialOrder и IsOrderedAddMonoid.

LaTeX

$$$\\text{IsOrderedAddMonoid}(\\mathrm{WithBot}(\\alpha))$ при $[AddCommMonoid \\alpha], [PartialOrder \\alpha], [IsOrderedAddMonoid \\alpha]$$$

Lean4

instance isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
    IsOrderedAddMonoid (WithBot α) :=
  { add_le_add_left := fun _ _ h c => add_le_add_left h c }

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