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 β:

• IsOrderedCancelMonoid and IsOrderedCancelAddMonoid.

Tags

filter, germ

instance Filter.Germ.instIsOrderedMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [CommMonoid β] [Preorder β] [IsOrderedMonoid β] : IsOrderedMonoid (l.Germ β)

instance Filter.Germ.instIsOrderedAddMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] : IsOrderedAddMonoid (l.Germ β)

instance Filter.Germ.instIsOrderedCancelMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [CommMonoid β] [Preorder β] [IsOrderedCancelMonoid β] : IsOrderedCancelMonoid (l.Germ β)

instance Filter.Germ.instIsOrderedAddCancelMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] : IsOrderedCancelAddMonoid (l.Germ β)

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 β)