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 β
:
Tags #
filter, germ
instance
Filter.Germ.instIsOrderedMonoid
{α : Type u_1}
{β : Type u_2}
{l : Filter α}
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
:
IsOrderedMonoid (l.Germ β)
instance
Filter.Germ.instIsOrderedAddMonoid
{α : Type u_1}
{β : Type u_2}
{l : Filter α}
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
:
IsOrderedAddMonoid (l.Germ β)
instance
Filter.Germ.instIsOrderedCancelMonoid
{α : Type u_1}
{β : Type u_2}
{l : Filter α}
[CommMonoid β]
[PartialOrder β]
[IsOrderedCancelMonoid β]
:
IsOrderedCancelMonoid (l.Germ β)
instance
Filter.Germ.instIsOrderedAddCancelMonoid
{α : Type u_1}
{β : Type u_2}
{l : Filter α}
[AddCommMonoid β]
[PartialOrder β]
[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 β)