Documentation

Mathlib.Algebra.Order.Monoid.WithTop

Adjoining top/bottom elements to ordered monoids. #

source
instance WithTop.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] :
OrderedAddCommMonoid (WithTop α)
Equations
source
instance WithTop.canonicallyOrderedAddCommMonoid {α : Type u} [CanonicallyOrderedAddCommMonoid α] :
CanonicallyOrderedAddCommMonoid (WithTop α)
Equations
  • WithTop.canonicallyOrderedAddCommMonoid = let __src := WithTop.orderBot; let __src_1 := WithTop.orderedAddCommMonoid; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
source
instance WithTop.instCanonicallyLinearOrderedAddCommMonoid {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] :
CanonicallyLinearOrderedAddCommMonoid (WithTop α)
Equations
  • One or more equations did not get rendered due to their size.
source
instance WithBot.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] :
OrderedAddCommMonoid (WithBot α)
Equations
  • WithBot.orderedAddCommMonoid = let __src := WithBot.partialOrder; let __src_1 := WithBot.addCommMonoid; OrderedAddCommMonoid.mk ⋯
source
instance WithBot.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] :
LinearOrderedAddCommMonoid (WithBot α)
Equations
  • One or more equations did not get rendered due to their size.