Adjoining top/bottom elements to ordered monoids.

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

Equations

• WithTop.orderedAddCommMonoid = { toAddCommMonoid := WithTop.addCommMonoid, toPartialOrder := WithTop.partialOrder, add_le_add_left := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• WithBot.orderedAddCommMonoid = { toAddCommMonoid := WithBot.addCommMonoid, toPartialOrder := WithBot.partialOrder, add_le_add_left := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.