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.instCanonicallyOrderedCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [CanonicallyOrderedCommMonoid β] : CanonicallyOrderedCommMonoid (l.Germ β)

Equations

• Filter.Germ.instCanonicallyOrderedCommMonoid = CanonicallyOrderedCommMonoid.mk ⋯ ⋯

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

Equations

• Filter.Germ.instCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯