Adjoining top/bottom elements to ordered monoids.

instance WithTop.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α)

Equations

• WithTop.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance WithTop.canonicallyOrderedAdd {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithTop α)

instance WithTop.instLinearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoid (WithTop α)

Equations

• WithTop.instLinearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance WithBot.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithBot α)

Equations

• WithBot.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance WithBot.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoid (WithBot α)

Equations

• WithBot.linearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯