Adjoining top/bottom elements to ordered monoids.

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

Equations

• WithTop.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance WithTop.canonicallyOrderedAddCommMonoid {α : Type u} [CanonicallyOrderedAddCommMonoid α] : CanonicallyOrderedAddCommMonoid (WithTop α)

Equations

• WithTop.canonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

instance WithTop.instCanonicallyLinearOrderedAddCommMonoid {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] : CanonicallyLinearOrderedAddCommMonoid (WithTop α)

Equations

• WithTop.instCanonicallyLinearOrderedAddCommMonoid = CanonicallyLinearOrderedAddCommMonoid.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 ⋯ ⋯ ⋯