Ordered monoid instances on the space of germs of a function at a filter

For each of the following structures we prove that if β has this structure, then so does Germ l β:

• OrderedCancelCommMonoid and OrderedCancelAddCommMonoid.

Tags

filter, germ

instance Filter.Germ.instOrderedCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommMonoid β] : OrderedCommMonoid (l.Germ β)

Equations

• Filter.Germ.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Filter.Germ.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommMonoid β] : OrderedAddCommMonoid (l.Germ β)

Equations

• Filter.Germ.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance Filter.Germ.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCancelCommMonoid β] : OrderedCancelCommMonoid (l.Germ β)

Equations

• Filter.Germ.instOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance Filter.Germ.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCancelAddCommMonoid β] : OrderedCancelAddCommMonoid (l.Germ β)

Equations

• Filter.Germ.instOrderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Filter.Germ.instCanonicallyOrderedMul {α : Type u_1} {β : Type u_2} {l : Filter α} [Mul β] [LE β] [CanonicallyOrderedMul β] : CanonicallyOrderedMul (l.Germ β)

instance Filter.Germ.instCanonicallyOrderedAdd {α : Type u_1} {β : Type u_2} {l : Filter α} [Add β] [LE β] [CanonicallyOrderedAdd β] : CanonicallyOrderedAdd (l.Germ β)