Documentation

Mathlib.Order.Filter.Germ.OrderedMonoid

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.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommMonoid β] :
Equations
theorem Filter.Germ.instOrderedAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommMonoid β] (f : l.Germ β) (g : l.Germ β) :
f g∀ (c : l.Germ β), c + f c + g
instance Filter.Germ.instOrderedCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommMonoid β] :
OrderedCommMonoid (l.Germ β)
Equations
Equations
theorem Filter.Germ.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCancelAddCommMonoid β] (f : l.Germ β) (g : l.Germ β) (h : l.Germ β) :
f + g f + hg h
Equations
theorem Filter.Germ.instCanonicallyOrderedAddCommMonoid.proof_3 {α : Type u_1} {β : Type u_2} {l : Filter α} [CanonicallyOrderedAddCommMonoid β] (x : l.Germ β) (y : l.Germ β) :
x x + y
Equations
theorem Filter.Germ.instCanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} {l : Filter α} [CanonicallyOrderedAddCommMonoid β] :
∀ {a b : l.Germ β}, a b∃ (c : l.Germ β), b = a + c
Equations