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 = { toCommMonoid := Filter.Germ.instCommMonoid, toPartialOrder := Filter.Germ.instPartialOrder, mul_le_mul_left := ⋯ }

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

Equations

• Filter.Germ.instOrderedAddCommMonoid = { toAddCommMonoid := Filter.Germ.instAddCommMonoid, toPartialOrder := Filter.Germ.instPartialOrder, add_le_add_left := ⋯ }

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

Equations

• Filter.Germ.instOrderedCancelCommMonoid = { toOrderedCommMonoid := Filter.Germ.instOrderedCommMonoid, le_of_mul_le_mul_left := ⋯ }

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

Equations

• Filter.Germ.instOrderedAddCancelCommMonoid = { toOrderedAddCommMonoid := Filter.Germ.instOrderedAddCommMonoid, le_of_add_le_add_left := ⋯ }

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