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

Equations

• Filter.Germ.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

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

• Filter.Germ.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

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

Equations

• Filter.Germ.instOrderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

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 + h → g ≤ h

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

Equations

• Filter.Germ.instOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

theorem Filter.Germ.instCanonicallyOrderedAddCommMonoid.proof_3 {α : Type u_1} {β : Type u_2} {l : Filter α} [CanonicallyOrderedAddCommMonoid β] (x : l.Germ β) (y : l.Germ β) : x ≤ x + y

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

Equations

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

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

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

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

Equations

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