# Germ of a function at a filter #

The germ of a function f : α → β at a filter l : Filter α is the equivalence class of f with respect to the equivalence relation EventuallyEq l: f ≈ g means ∀ᶠ x in l, f x = g x.

## Main definitions #

We define

• Filter.Germ l β to be the space of germs of functions α → β at a filter l : Filter α;
• coercion from α → β to Germ l β: (f : Germ l β) is the germ of f : α → β at l : Filter α; this coercion is declared as CoeTC;
• (const l c : Germ l β) is the germ of the constant function fun x : α ↦ c at a filter l;
• coercion from β to Germ l β: (↑c : Germ l β) is the germ of the constant function fun x : α ↦ c at a filter l; this coercion is declared as CoeTC;
• map (F : β → γ) (f : Germ l β) to be the composition of a function F and a germ f;
• map₂ (F : β → γ → δ) (f : Germ l β) (g : Germ l γ) to be the germ of fun x ↦ F (f x) (g x) at l;
• f.Tendsto lb: we say that a germ f : Germ l β tends to a filter lb if its representatives tend to lb along l;
• f.compTendsto g hg and f.compTendsto' g hg: given f : Germ l β and a function g : γ → α (resp., a germ g : Germ lc α), if g tends to l along lc, then the composition f ∘ g is a well-defined germ at lc;
• Germ.liftPred, Germ.liftRel: lift a predicate or a relation to the space of germs: (f : Germ l β).liftPred p means ∀ᶠ x in l, p (f x), and similarly for a relation.

We also define map (F : β → γ) : Germ l β → Germ l γ sending each germ f to F ∘ f.

For each of the following structures we prove that if β has this structure, then so does Germ l β:

• one-operation algebraic structures up to CommGroup;
• MulZeroClass, Distrib, Semiring, CommSemiring, Ring, CommRing;
• MulAction, DistribMulAction, Module;
• Preorder, PartialOrder, and Lattice structures, as well as BoundedOrder;
• OrderedCancelCommMonoid and OrderedCancelAddCommMonoid.

## Tags #

filter, germ

theorem Filter.const_eventuallyEq' {α : Type u_1} {β : Type u_2} {l : } [l.NeBot] {a : β} {b : β} :
(∀ᶠ (x : α) in l, a = b) a = b
theorem Filter.const_eventuallyEq {α : Type u_1} {β : Type u_2} {l : } [l.NeBot] {a : β} {b : β} :
((fun (x : α) => a) =ᶠ[l] fun (x : α) => b) a = b
def Filter.germSetoid {α : Type u_1} (l : ) (β : Type u_5) :
Setoid (αβ)

Setoid used to define the space of germs.

Equations
• l.germSetoid β = { r := l.EventuallyEq, iseqv := }
Instances For
def Filter.Germ {α : Type u_1} (l : ) (β : Type u_5) :
Type (max u_1 u_5)

The space of germs of functions α → β at a filter l.

Equations
Instances For
def Filter.productSetoid {α : Type u_1} (l : ) (ε : αType u_5) :
Setoid ((a : α) → ε a)

Setoid used to define the filter product. This is a dependent version of Filter.germSetoid.

Equations
• l.productSetoid ε = { r := fun (f g : (a : α) → ε a) => ∀ᶠ (a : α) in l, f a = g a, iseqv := }
Instances For
def Filter.Product {α : Type u_1} (l : ) (ε : αType u_5) :
Type (max u_1 u_5)

The filter product (a : α) → ε a at a filter l. This is a dependent version of Filter.Germ.

Equations
Instances For
instance Filter.Product.coeTC {α : Type u_1} {l : } {ε : αType u_5} :
CoeTC ((a : α) → ε a) (l.Product ε)
Equations
• Filter.Product.coeTC = { coe := Quotient.mk' }
instance Filter.Product.instInhabited {α : Type u_1} {l : } {ε : αType u_5} [(a : α) → Inhabited (ε a)] :
Inhabited (l.Product ε)
Equations
• Filter.Product.instInhabited = { default := Quotient.mk' fun (a : α) => default }
def Filter.Germ.ofFun {α : Type u_1} {β : Type u_2} {l : } :
(αβ)l.Germ β
Equations
• Filter.Germ.ofFun = Quotient.mk'
Instances For
instance Filter.Germ.instCoeTCForall {α : Type u_1} {β : Type u_2} {l : } :
CoeTC (αβ) (l.Germ β)
Equations
• Filter.Germ.instCoeTCForall = { coe := Filter.Germ.ofFun }
def Filter.Germ.const {α : Type u_1} {β : Type u_2} {l : } (b : β) :
l.Germ β
Equations
• b = fun (x : α) => b
Instances For
instance Filter.Germ.coeTC {α : Type u_1} {β : Type u_2} {l : } :
CoeTC β (l.Germ β)
Equations
• Filter.Germ.coeTC = { coe := Filter.Germ.const }
def Filter.Germ.IsConstant {α : Type u_1} {β : Type u_2} {l : } (P : l.Germ β) :

A germ P of functions α → β is constant w.r.t. l.

Equations
Instances For
theorem Filter.Germ.isConstant_coe {α : Type u_1} {β : Type u_2} {f : αβ} {l : } {b : β} (h : ∀ (x' : α), f x' = b) :
(f).IsConstant
@[simp]
theorem Filter.Germ.isConstant_coe_const {α : Type u_1} {β : Type u_2} {l : } {b : β} :
(fun (x : α) => b).IsConstant
theorem Filter.Germ.isConstant_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : αβ} {g : βγ} (h : (f).IsConstant) :
((g f)).IsConstant

If f : α → β is constant w.r.t. l and g : β → γ, then g ∘ f : α → γ also is.

@[simp]
theorem Filter.Germ.quot_mk_eq_coe {α : Type u_1} {β : Type u_2} (l : ) (f : αβ) :
Quot.mk Setoid.r f = f
@[simp]
theorem Filter.Germ.mk'_eq_coe {α : Type u_1} {β : Type u_2} (l : ) (f : αβ) :
= f
theorem Filter.Germ.inductionOn {α : Type u_1} {β : Type u_2} {l : } (f : l.Germ β) {p : l.Germ βProp} (h : ∀ (f : αβ), p f) :
p f
theorem Filter.Germ.inductionOn₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : l.Germ β) (g : l.Germ γ) {p : l.Germ βl.Germ γProp} (h : ∀ (f : αβ) (g : αγ), p f g) :
p f g
theorem Filter.Germ.inductionOn₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } (f : l.Germ β) (g : l.Germ γ) (h : l.Germ δ) {p : l.Germ βl.Germ γl.Germ δProp} (H : ∀ (f : αβ) (g : αγ) (h : αδ), p f g h) :
p f g h
def Filter.Germ.map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } {lc : } (F : (αβ)γδ) (hF : (l.EventuallyEq lc.EventuallyEq) F F) :
l.Germ βlc.Germ δ

Given a map F : (α → β) → (γ → δ) that sends functions eventually equal at l to functions eventually equal at lc, returns a map from Germ l β to Germ lc δ.

Equations
Instances For
def Filter.Germ.liftOn {α : Type u_1} {β : Type u_2} {l : } {γ : Sort u_5} (f : l.Germ β) (F : (αβ)γ) (hF : (l.EventuallyEq fun (x x_1 : γ) => x = x_1) F F) :
γ

Given a germ f : Germ l β and a function F : (α → β) → γ sending eventually equal functions to the same value, returns the value F takes on functions having germ f at l.

Equations
Instances For
@[simp]
theorem Filter.Germ.map'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } {lc : } (F : (αβ)γδ) (hF : (l.EventuallyEq lc.EventuallyEq) F F) (f : αβ) :
Filter.Germ.map' F hF f = (F f)
@[simp]
theorem Filter.Germ.coe_eq {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g : αβ} :
f = g f =ᶠ[l] g
theorem Filter.EventuallyEq.germ_eq {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g : αβ} :
f =ᶠ[l] gf = g

Alias of the reverse direction of Filter.Germ.coe_eq.

def Filter.Germ.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (op : βγ) :
l.Germ βl.Germ γ

Lift a function β → γ to a function Germ l β → Germ l γ.

Equations
Instances For
@[simp]
theorem Filter.Germ.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (op : βγ) (f : αβ) :
Filter.Germ.map op f = (op f)
@[simp]
theorem Filter.Germ.map_id {α : Type u_1} {β : Type u_2} {l : } :
= id
theorem Filter.Germ.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } (op₁ : γδ) (op₂ : βγ) (f : l.Germ β) :
Filter.Germ.map op₁ (Filter.Germ.map op₂ f) = Filter.Germ.map (op₁ op₂) f
def Filter.Germ.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } (op : βγδ) :
l.Germ βl.Germ γl.Germ δ

Lift a binary function β → γ → δ to a function Germ l β → Germ l γ → Germ l δ.

Equations
• = Quotient.map₂' (fun (f : αβ) (g : αγ) (x : α) => op (f x) (g x))
Instances For
@[simp]
theorem Filter.Germ.map₂_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : } (op : βγδ) (f : αβ) (g : αγ) :
Filter.Germ.map₂ op f g = fun (x : α) => op (f x) (g x)
def Filter.Germ.Tendsto {α : Type u_1} {β : Type u_2} {l : } (f : l.Germ β) (lb : ) :

A germ at l of maps from α to β tends to lb : Filter β if it is represented by a map which tends to lb along l.

Equations
Instances For
@[simp]
theorem Filter.Germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {lb : } :
(f).Tendsto lb Filter.Tendsto f l lb
theorem Filter.Tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {lb : } :
Filter.Tendsto f l lb(f).Tendsto lb

Alias of the reverse direction of Filter.Germ.coe_tendsto.

def Filter.Germ.compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : l.Germ β) {lc : } (g : lc.Germ α) (hg : g.Tendsto l) :
lc.Germ β

Given two germs f : Germ l β, and g : Germ lc α, where l : Filter α, if g tends to l, then the composition f ∘ g is well-defined as a germ at lc.

Equations
• f.compTendsto' g hg = f.liftOn (fun (f : αβ) => )
Instances For
@[simp]
theorem Filter.Germ.coe_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : αβ) {lc : } {g : lc.Germ α} (hg : g.Tendsto l) :
(f).compTendsto' g hg =
def Filter.Germ.compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : l.Germ β) {lc : } (g : γα) (hg : Filter.Tendsto g lc l) :
lc.Germ β

Given a germ f : Germ l β and a function g : γ → α, where l : Filter α, if g tends to l along lc : Filter γ, then the composition f ∘ g is well-defined as a germ at lc.

Equations
• f.compTendsto g hg = f.compTendsto' g
Instances For
@[simp]
theorem Filter.Germ.coe_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : αβ) {lc : } {g : γα} (hg : Filter.Tendsto g lc l) :
(f).compTendsto g hg = (f g)
@[simp]
theorem Filter.Germ.compTendsto'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (f : l.Germ β) {lc : } {g : γα} (hg : Filter.Tendsto g lc l) :
f.compTendsto' g = f.compTendsto g hg
theorem Filter.Germ.Filter.Tendsto.congr_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βγ} {g : βγ} {l : } {l' : } (h : f =ᶠ[l'] g) {φ : αβ} (hφ : Filter.Tendsto φ l l') :
(f φ) = (g φ)
theorem Filter.Germ.isConstant_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : αβ} {lc : } {g : γα} (hf : (f).IsConstant) (hg : Filter.Tendsto g lc l) :
((f g)).IsConstant
theorem Filter.Germ.isConstant_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {f : l.Germ β} {lc : } {g : γα} (hf : f.IsConstant) (hg : Filter.Tendsto g lc l) :
(f.compTendsto g hg).IsConstant

If a germ f : Germ l β is constant, where l : Filter α, and a function g : γ → α tends to l along lc : Filter γ, the germ of the composition f ∘ g is also constant.

@[simp]
theorem Filter.Germ.const_inj {α : Type u_1} {β : Type u_2} {l : } [l.NeBot] {a : β} {b : β} :
a = b a = b
@[simp]
theorem Filter.Germ.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : ) (a : β) (f : βγ) :
= (f a)
@[simp]
theorem Filter.Germ.map₂_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : ) (b : β) (c : γ) (f : βγδ) :
Filter.Germ.map₂ f b c = (f b c)
@[simp]
theorem Filter.Germ.const_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (b : β) {lc : } {g : γα} (hg : Filter.Tendsto g lc l) :
(b).compTendsto g hg = b
@[simp]
theorem Filter.Germ.const_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (b : β) {lc : } {g : lc.Germ α} (hg : g.Tendsto l) :
(b).compTendsto' g hg = b
def Filter.Germ.LiftPred {α : Type u_1} {β : Type u_2} {l : } (p : βProp) (f : l.Germ β) :

Lift a predicate on β to Germ l β.

Equations
• = f.liftOn (fun (f : αβ) => ∀ᶠ (x : α) in l, p (f x))
Instances For
@[simp]
theorem Filter.Germ.liftPred_coe {α : Type u_1} {β : Type u_2} {l : } {p : βProp} {f : αβ} :
∀ᶠ (x : α) in l, p (f x)
theorem Filter.Germ.liftPred_const {α : Type u_1} {β : Type u_2} {l : } {p : βProp} {x : β} (hx : p x) :
@[simp]
theorem Filter.Germ.liftPred_const_iff {α : Type u_1} {β : Type u_2} {l : } [l.NeBot] {p : βProp} {x : β} :
p x
def Filter.Germ.LiftRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } (r : βγProp) (f : l.Germ β) (g : l.Germ γ) :

Lift a relation r : β → γ → Prop to Germ l β → Germ l γ → Prop.

Equations
• = Quotient.liftOn₂' f g (fun (f : αβ) (g : αγ) => ∀ᶠ (x : α) in l, r (f x) (g x))
Instances For
@[simp]
theorem Filter.Germ.liftRel_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {r : βγProp} {f : αβ} {g : αγ} :
Filter.Germ.LiftRel r f g ∀ᶠ (x : α) in l, r (f x) (g x)
theorem Filter.Germ.liftRel_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } {r : βγProp} {x : β} {y : γ} (h : r x y) :
@[simp]
theorem Filter.Germ.liftRel_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : } [l.NeBot] {r : βγProp} {x : β} {y : γ} :
Filter.Germ.LiftRel r x y r x y
instance Filter.Germ.instInhabited {α : Type u_1} {β : Type u_2} {l : } [] :
Inhabited (l.Germ β)
Equations
• Filter.Germ.instInhabited = { default := default }
instance Filter.Germ.instAdd {α : Type u_1} {l : } {M : Type u_5} [Add M] :
Equations
instance Filter.Germ.instMul {α : Type u_1} {l : } {M : Type u_5} [Mul M] :
Mul (l.Germ M)
Equations
@[simp]
theorem Filter.Germ.coe_add {α : Type u_1} {l : } {M : Type u_5} [Add M] (f : αM) (g : αM) :
(f + g) = f + g
@[simp]
theorem Filter.Germ.coe_mul {α : Type u_1} {l : } {M : Type u_5} [Mul M] (f : αM) (g : αM) :
(f * g) = f * g
instance Filter.Germ.instZero {α : Type u_1} {l : } {M : Type u_5} [Zero M] :
Zero (l.Germ M)
Equations
• Filter.Germ.instZero = { zero := 0 }
instance Filter.Germ.instOne {α : Type u_1} {l : } {M : Type u_5} [One M] :
One (l.Germ M)
Equations
• Filter.Germ.instOne = { one := 1 }
@[simp]
theorem Filter.Germ.coe_zero {α : Type u_1} {l : } {M : Type u_5} [Zero M] :
0 = 0
@[simp]
theorem Filter.Germ.coe_one {α : Type u_1} {l : } {M : Type u_5} [One M] :
1 = 1
theorem Filter.Germ.instAddSemigroup.proof_1 {α : Type u_2} {l : } {M : Type u_1} [] (a : l.Germ M) (b : l.Germ M) (c : l.Germ M) :
a + b + c = a + (b + c)
instance Filter.Germ.instAddSemigroup {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
instance Filter.Germ.instSemigroup {α : Type u_1} {l : } {M : Type u_5} [] :
Semigroup (l.Germ M)
Equations
• Filter.Germ.instSemigroup =
instance Filter.Germ.instAddCommSemigroup {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
theorem Filter.Germ.instAddCommSemigroup.proof_1 {α : Type u_1} {l : } {M : Type u_2} [] (q₁ : Quotient (l.germSetoid M)) (q₂ : Quotient (l.germSetoid M)) :
q₁ + q₂ = q₂ + q₁
instance Filter.Germ.instCommSemigroup {α : Type u_1} {l : } {M : Type u_5} [] :
CommSemigroup (l.Germ M)
Equations
• Filter.Germ.instCommSemigroup =
instance Filter.Germ.instIsAddLeftCancel {α : Type u_1} {l : } {M : Type u_5} [Add M] [] :
Equations
• =
instance Filter.Germ.instIsLeftCancelMul {α : Type u_1} {l : } {M : Type u_5} [Mul M] [] :
IsLeftCancelMul (l.Germ M)
Equations
• =
instance Filter.Germ.instIsAddRightCancel {α : Type u_1} {l : } {M : Type u_5} [Add M] [] :
Equations
• =
instance Filter.Germ.instIsRightCancelMul {α : Type u_1} {l : } {M : Type u_5} [Mul M] [] :
IsRightCancelMul (l.Germ M)
Equations
• =
instance Filter.Germ.instIsAddCancel {α : Type u_1} {l : } {M : Type u_5} [Add M] [] :
Equations
• =
instance Filter.Germ.instIsCancelMul {α : Type u_1} {l : } {M : Type u_5} [Mul M] [] :
IsCancelMul (l.Germ M)
Equations
• =
theorem Filter.Germ.instAddLeftCancelSemigroup.proof_1 {α : Type u_2} {l : } {M : Type u_1} :
∀ (x x_1 x_2 : l.Germ M), x + x_1 = x + x_2x_1 = x_2
instance Filter.Germ.instAddLeftCancelSemigroup {α : Type u_1} {l : } {M : Type u_5} :
Equations
instance Filter.Germ.instLeftCancelSemigroup {α : Type u_1} {l : } {M : Type u_5} :
Equations
• Filter.Germ.instLeftCancelSemigroup =
instance Filter.Germ.instAddRightCancelSemigroup {α : Type u_1} {l : } {M : Type u_5} :
Equations
theorem Filter.Germ.instAddRightCancelSemigroup.proof_1 {α : Type u_2} {l : } {M : Type u_1} :
∀ (x x_1 x_2 : l.Germ M), x + x_1 = x_2 + x_1x = x_2
instance Filter.Germ.instRightCancelSemigroup {α : Type u_1} {l : } {M : Type u_5} :
Equations
• Filter.Germ.instRightCancelSemigroup =
theorem Filter.Germ.instAddZeroClass.proof_1 {α : Type u_1} {l : } {M : Type u_2} [] (q : Quotient (l.germSetoid M)) :
0 + q = q
instance Filter.Germ.instAddZeroClass {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
theorem Filter.Germ.instAddZeroClass.proof_2 {α : Type u_1} {l : } {M : Type u_2} [] (q : Quotient (l.germSetoid M)) :
q + 0 = q
instance Filter.Germ.instMulOneClass {α : Type u_1} {l : } {M : Type u_5} [] :
MulOneClass (l.Germ M)
Equations
• Filter.Germ.instMulOneClass =
instance Filter.Germ.instVAdd {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [VAdd M G] :
Equations
instance Filter.Germ.instSMul {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [SMul M G] :
SMul M (l.Germ G)
Equations
instance Filter.Germ.instPow {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [Pow G M] :
Pow (l.Germ G) M
Equations
• Filter.Germ.instPow = { pow := fun (f : l.Germ G) (n : M) => Filter.Germ.map (fun (x : G) => x ^ n) f }
@[simp]
theorem Filter.Germ.coe_vadd {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [VAdd M G] (n : M) (f : αG) :
(n +ᵥ f) = n +ᵥ f
@[simp]
theorem Filter.Germ.coe_smul {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [SMul M G] (n : M) (f : αG) :
(n f) = n f
@[simp]
theorem Filter.Germ.const_vadd {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [VAdd M G] (n : M) (a : G) :
(n +ᵥ a) = n +ᵥ a
@[simp]
theorem Filter.Germ.const_smul {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [SMul M G] (n : M) (a : G) :
(n a) = n a
@[simp]
theorem Filter.Germ.coe_nsmul {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [SMul M G] (f : αG) (n : M) :
(n f) = n f
@[simp]
theorem Filter.Germ.coe_pow {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [Pow G M] (f : αG) (n : M) :
(f ^ n) = f ^ n
@[simp]
theorem Filter.Germ.const_nsmul {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [SMul M G] (a : G) (n : M) :
(n a) = n a
@[simp]
theorem Filter.Germ.const_pow {α : Type u_1} {l : } {M : Type u_5} {G : Type u_6} [Pow G M] (a : G) (n : M) :
(a ^ n) = a ^ n
theorem Filter.Germ.instAddMonoid.proof_2 {α : Type u_1} {l : } {M : Type u_2} [] :
0 = 0
theorem Filter.Germ.instAddMonoid.proof_8 {α : Type u_2} {l : } {M : Type u_1} [] (n : ) (x : l.Germ M) :
AddMonoid.nsmul (n + 1) x = + x
theorem Filter.Germ.instAddMonoid.proof_7 {α : Type u_2} {l : } {M : Type u_1} [] (x : l.Germ M) :
= 0
theorem Filter.Germ.instAddMonoid.proof_6 {α : Type u_2} {l : } {M : Type u_1} [] (a : l.Germ M) :
a + 0 = a
theorem Filter.Germ.instAddMonoid.proof_1 {α : Type u_1} {l : } {M : Type u_2} :
theorem Filter.Germ.instAddMonoid.proof_3 {α : Type u_1} {l : } {M : Type u_2} [] :
∀ (x x_1 : αM), (x + x_1) = (x + x_1)
theorem Filter.Germ.instAddMonoid.proof_4 {α : Type u_1} {l : } {M : Type u_2} [] :
∀ (x : αM) (x_1 : ), (x_1 x) = (x_1 x)
theorem Filter.Germ.instAddMonoid.proof_5 {α : Type u_2} {l : } {M : Type u_1} [] (a : l.Germ M) :
0 + a = a
instance Filter.Germ.instAddMonoid {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
instance Filter.Germ.instMonoid {α : Type u_1} {l : } {M : Type u_5} [] :
Monoid (l.Germ M)
Equations
theorem Filter.Germ.coeAddHom.proof_1 {α : Type u_1} {M : Type u_2} [] (l : ) :
0 = 0
def Filter.Germ.coeAddHom {α : Type u_1} {M : Type u_5} [] (l : ) :
(αM) →+ l.Germ M

Coercion from functions to germs as an additive monoid homomorphism.

Equations
• = { toFun := Filter.Germ.ofFun, map_zero' := , map_add' := }
Instances For
theorem Filter.Germ.coeAddHom.proof_2 {α : Type u_1} {M : Type u_2} [] (l : ) :
∀ (x x_1 : αM), { toFun := Filter.Germ.ofFun, map_zero' := }.toFun (x + x_1) = { toFun := Filter.Germ.ofFun, map_zero' := }.toFun (x + x_1)
def Filter.Germ.coeMulHom {α : Type u_1} {M : Type u_5} [] (l : ) :
(αM) →* l.Germ M

Coercion from functions to germs as a monoid homomorphism.

Equations
• = { toFun := Filter.Germ.ofFun, map_one' := , map_mul' := }
Instances For
@[simp]
theorem Filter.Germ.coe_coeAddHom {α : Type u_1} {l : } {M : Type u_5} [] :
= Filter.Germ.ofFun
@[simp]
theorem Filter.Germ.coe_coeMulHom {α : Type u_1} {l : } {M : Type u_5} [] :
= Filter.Germ.ofFun
instance Filter.Germ.instAddCommMonoid {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
theorem Filter.Germ.instAddCommMonoid.proof_1 {α : Type u_2} {l : } {M : Type u_1} [] (a : l.Germ M) (b : l.Germ M) :
a + b = b + a
instance Filter.Germ.instCommMonoid {α : Type u_1} {l : } {M : Type u_5} [] :
CommMonoid (l.Germ M)
Equations
• Filter.Germ.instCommMonoid =
instance Filter.Germ.instNatCast {α : Type u_1} {l : } {M : Type u_5} [] :
NatCast (l.Germ M)
Equations
• Filter.Germ.instNatCast = { natCast := fun (n : ) => n }
@[simp]
theorem Filter.Germ.natCast_def {α : Type u_1} {l : } {M : Type u_5} [] (n : ) :
(fun (x : α) => n) = n
@[simp]
theorem Filter.Germ.const_nat {α : Type u_1} {l : } {M : Type u_5} [] (n : ) :
n = n
@[simp]
theorem Filter.Germ.coe_ofNat {α : Type u_1} {l : } {M : Type u_5} [] (n : ) [n.AtLeastTwo] :
() =
@[simp]
theorem Filter.Germ.const_ofNat {α : Type u_1} {l : } {M : Type u_5} [] (n : ) [n.AtLeastTwo] :
() =
instance Filter.Germ.instIntCast {α : Type u_1} {l : } {M : Type u_5} [] :
IntCast (l.Germ M)
Equations
• Filter.Germ.instIntCast = { intCast := fun (n : ) => n }
@[simp]
theorem Filter.Germ.intCast_def {α : Type u_1} {l : } {M : Type u_5} [] (n : ) :
(fun (x : α) => n) = n
@[deprecated Filter.Germ.natCast_def]
theorem Filter.Germ.coe_nat {α : Type u_1} {l : } {M : Type u_5} [] (n : ) :
(fun (x : α) => n) = n

Alias of Filter.Germ.natCast_def.

@[deprecated Filter.Germ.intCast_def]
theorem Filter.Germ.coe_int {α : Type u_1} {l : } {M : Type u_5} [] (n : ) :
(fun (x : α) => n) = n

Alias of Filter.Germ.intCast_def.

instance Filter.Germ.instAddMonoidWithOne {α : Type u_1} {l : } {M : Type u_5} [] :
Equations
instance Filter.Germ.instAddCommMonoidWithOne {α : Type u_1} {l : } {M : Type u_5} :
Equations
instance Filter.Germ.instNeg {α : Type u_1} {l : } {G : Type u_6} [Neg G] :
Neg (l.Germ G)
Equations
instance Filter.Germ.instInv {α : Type u_1} {l : } {G : Type u_6} [Inv G] :
Inv (l.Germ G)
Equations
@[simp]
theorem Filter.Germ.coe_neg {α : Type u_1} {l : } {G : Type u_6} [Neg G] (f : αG) :
(-f) = -f
@[simp]
theorem Filter.Germ.coe_inv {α : Type u_1} {l : } {G : Type u_6} [Inv G] (f : αG) :
f⁻¹ = (f)⁻¹
@[simp]
theorem Filter.Germ.const_neg {α : Type u_1} {l : } {G : Type u_6} [Neg G] (a : G) :
(-a) = -a
@[simp]
theorem Filter.Germ.const_inv {α : Type u_1} {l : } {G : Type u_6} [Inv G] (a : G) :
a⁻¹ = (a)⁻¹
instance Filter.Germ.instSub {α : Type u_1} {l : } {M : Type u_5} [Sub M] :
Sub (l.Germ M)
Equations
instance Filter.Germ.instDiv {α : Type u_1} {l : } {M : Type u_5} [Div M] :
Div (l.Germ M)
Equations
@[simp]
theorem Filter.Germ.coe_sub {α : Type u_1} {l : } {M : Type u_5} [Sub M] (f : αM) (g : αM) :
(f - g) = f - g
@[simp]
theorem Filter.Germ.coe_div {α : Type u_1} {l : } {M : Type u_5} [Div M] (f : αM) (g : αM) :
(f / g) = f / g
@[simp]
theorem Filter.Germ.const_sub {α : Type u_1} {l : } {M : Type u_5} [Sub M] (a : M) (b : M) :
(a - b) = a - b
@[simp]
theorem Filter.Germ.const_div {α : Type u_1} {l : } {M : Type u_5} [Div M] (a : M) (b : M) :
(a / b) = a / b
theorem Filter.Germ.instInvolutiveNeg.proof_1 {α : Type u_1} {l : } {G : Type u_2} [] (q : Quotient (l.germSetoid G)) :
- -q = q
instance Filter.Germ.instInvolutiveNeg {α : Type u_1} {l : } {G : Type u_6} [] :
InvolutiveNeg (l.Germ G)
Equations
• Filter.Germ.instInvolutiveNeg =
instance Filter.Germ.instInvolutiveInv {α : Type u_1} {l : } {G : Type u_6} [] :
InvolutiveInv (l.Germ G)
Equations
• Filter.Germ.instInvolutiveInv =
instance Filter.Germ.instHasDistribNeg {α : Type u_1} {l : } {G : Type u_6} [Mul G] [] :
HasDistribNeg (l.Germ G)
Equations
• Filter.Germ.instHasDistribNeg =
theorem Filter.Germ.instNegZeroClass.proof_1 {α : Type u_1} {l : } {G : Type u_2} [] :
((fun (x : αG) => Neg.neg x) fun (x : α) => 0) = fun (x : α) => 0
instance Filter.Germ.instNegZeroClass {α : Type u_1} {l : } {G : Type u_6} [] :
NegZeroClass (l.Germ G)
Equations
• Filter.Germ.instNegZeroClass =
instance Filter.Germ.instInvOneClass {α : Type u_1} {l : } {G : Type u_6} [] :
InvOneClass (l.Germ G)
Equations
• Filter.Germ.instInvOneClass =
theorem Filter.Germ.subNegMonoid.proof_2 {α : Type u_1} {l : } {G : Type u_2} [] (q : Quotient (l.germSetoid G)) :
(fun (z : ) (f : l.Germ G) => z f) 0 q = 0
theorem Filter.Germ.subNegMonoid.proof_1 {α : Type u_1} {l : } {G : Type u_2} [] (q₁ : Quotient (l.germSetoid G)) (q₂ : Quotient (l.germSetoid G)) :
q₁ - q₂ = q₁ + -q₂
theorem Filter.Germ.subNegMonoid.proof_3 {α : Type u_1} {l : } {G : Type u_2} [] :
∀ (x : ) (q : Quotient (l.germSetoid G)), (fun (z : ) (f : l.Germ G) => z f) (Int.ofNat x.succ) q = (fun (z : ) (f : l.Germ G) => z f) () q + q
theorem Filter.Germ.subNegMonoid.proof_4 {α : Type u_1} {l : } {G : Type u_2} [] :
∀ (x : ) (q : Quotient (l.germSetoid G)), (fun (z : ) (f : l.Germ G) => z f) () q = -(fun (z : ) (f : l.Germ G) => z f) (x.succ) q
instance Filter.Germ.subNegMonoid {α : Type u_1} {l : } {G : Type u_6} [] :
SubNegMonoid (l.Germ G)
Equations
instance Filter.Germ.instDivInvMonoid {α : Type u_1} {l : } {G : Type u_6} [] :
DivInvMonoid (l.Germ G)
Equations
• Filter.Germ.instDivInvMonoid = DivInvMonoid.mk (fun (z : ) (f : l.Germ G) => f ^ z)
theorem Filter.Germ.instDivisionAddMonoid.proof_2 {α : Type u_2} {l : } {G : Type u_1} (x : l.Germ G) (y : l.Germ G) :
-(x + y) = -y + -x
instance Filter.Germ.instDivisionAddMonoid {α : Type u_1} {l : } {G : Type u_6} :
Equations
theorem Filter.Germ.instDivisionAddMonoid.proof_3 {α : Type u_2} {l : } {G : Type u_1} (x : l.Germ G) (y : l.Germ G) :
x + y = 0-x = y
theorem Filter.Germ.instDivisionAddMonoid.proof_1 {α : Type u_2} {l : } {G : Type u_1} (a : l.Germ G) :
- -a = a
instance Filter.Germ.instDivisionMonoid {α : Type u_1} {l : } {G : Type u_6} [] :
DivisionMonoid (l.Germ G)
Equations
• Filter.Germ.instDivisionMonoid =
theorem Filter.Germ.instAddGroup.proof_1 {α : Type u_1} {l : } {G : Type u_2} [] (q : Quotient (l.germSetoid G)) :
-q + q = 0
instance Filter.Germ.instAddGroup {α : Type u_1} {l : } {G : Type u_6} [] :
Equations
instance Filter.Germ.instGroup {α : Type u_1} {l : } {G : Type u_6} [] :
Group (l.Germ G)
Equations
• Filter.Germ.instGroup =
instance Filter.Germ.instAddCommGroup {α : Type u_1} {l : } {G : Type u_6} [] :
Equations
theorem Filter.Germ.instAddCommGroup.proof_1 {α : Type u_2} {l : } {G : Type u_1} [] (a : l.Germ G) (b : l.Germ G) :
a + b = b + a
instance Filter.Germ.instCommGroup {α : Type u_1} {l : } {G : Type u_6} [] :
CommGroup (l.Germ G)
Equations
• Filter.Germ.instCommGroup =
instance Filter.Germ.instAddGroupWithOne {α : Type u_1} {l : } {G : Type u_6} [] :
Equations
instance Filter.Germ.instNontrivial {α : Type u_1} {l : } {R : Type u_5} [] [l.NeBot] :
Nontrivial (l.Germ R)
Equations
• =
instance Filter.Germ.instMulZeroClass {α : Type u_1} {l : } {R : Type u_5} [] :
MulZeroClass (l.Germ R)
Equations
• Filter.Germ.instMulZeroClass =
instance Filter.Germ.instMulZeroOneClass {α : Type u_1} {l : } {R : Type u_5} [] :
MulZeroOneClass (l.Germ R)
Equations
instance Filter.Germ.instMonoidWithZero {α : Type u_1} {l : } {R : Type u_5} [] :
MonoidWithZero (l.Germ R)
Equations
instance Filter.Germ.instDistrib {α : Type u_1} {l : } {R : Type u_5} [] :
Distrib (l.Germ R)
Equations
• Filter.Germ.instDistrib =
instance Filter.Germ.instNonUnitalNonAssocSemiring {α : Type u_1} {l : } {R : Type u_5} :
Equations
• One or more equations did not get rendered due to their size.
instance Filter.Germ.instNonUnitalSemiring {α : Type u_1} {l : } {R : Type u_5} :
Equations
• Filter.Germ.instNonUnitalSemiring =
instance Filter.Germ.instNonAssocSemiring {α : Type u_1} {l : } {R : Type u_5} [] :
NonAssocSemiring (l.Germ R)
Equations
• One or more equations did not get rendered due to their size.
instance Filter.Germ.instNonUnitalNonAssocRing {α : Type u_1} {l : } {R : Type u_5} :
Equations
instance Filter.Germ.instNonUnitalRing {α : Type u_1} {l : } {R : Type u_5} [] :
NonUnitalRing (l.Germ R)
Equations
• Filter.Germ.instNonUnitalRing =
instance Filter.Germ.instNonAssocRing {α : Type u_1} {l : } {R : Type u_5} [] :
NonAssocRing (l.Germ R)
Equations
• One or more equations did not get rendered due to their size.
instance Filter.Germ.instSemiring {α : Type u_1} {l : } {R : Type u_5} [] :
Semiring (l.Germ R)
Equations
• One or more equations did not get rendered due to their size.
instance Filter.Germ.instRing {α : Type u_1} {l : } {R : Type u_5} [Ring R] :
Ring (l.Germ R)
Equations
• One or more equations did not get rendered due to their size.
instance Filter.Germ.instNonUnitalCommSemiring {α : Type u_1} {l : } {R : Type u_5} :
Equations
• Filter.Germ.instNonUnitalCommSemiring =
instance Filter.Germ.instCommSemiring {α : Type u_1} {l : } {R : Type u_5} [] :
CommSemiring (l.Germ R)
Equations
• Filter.Germ.instCommSemiring =
instance Filter.Germ.instNonUnitalCommRing {α : Type u_1} {l : } {R : Type u_5} :
Equations
instance Filter.Germ.instCommRing {α : Type u_1} {l : } {R : Type u_5} [] :
CommRing (l.Germ R)
Equations
• Filter.Germ.instCommRing =
def Filter.Germ.coeRingHom {α : Type u_1} {R : Type u_5} [] (l : ) :
(αR) →+* l.Germ R

Coercion (α → R) → Germ l R as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Filter.Germ.coe_coeRingHom {α : Type u_1} {l : } {R : Type u_5} [] :
= Filter.Germ.ofFun
instance Filter.Germ.instVAdd' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [VAdd M β] :
Equations
instance Filter.Germ.instSMul' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [SMul M β] :
SMul (l.Germ M) (l.Germ β)
Equations
@[simp]
theorem Filter.Germ.coe_vadd' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [VAdd M β] (c : αM) (f : αβ) :
(c +ᵥ f) = c +ᵥ f
@[simp]
theorem Filter.Germ.coe_smul' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [SMul M β] (c : αM) (f : αβ) :
(c f) = c f
theorem Filter.Germ.instAddAction.proof_1 {α : Type u_2} {β : Type u_1} {l : } {M : Type u_3} [] [] (f : l.Germ β) :
0 +ᵥ f = f
instance Filter.Germ.instAddAction {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [] [] :
Equations
theorem Filter.Germ.instAddAction.proof_2 {α : Type u_2} {β : Type u_1} {l : } {M : Type u_3} [] [] (c₁ : M) (c₂ : M) (f : l.Germ β) :
c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)
instance Filter.Germ.instMulAction {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [] [] :
MulAction M (l.Germ β)
Equations
• Filter.Germ.instMulAction =
theorem Filter.Germ.instAddAction'.proof_2 {α : Type u_2} {β : Type u_3} {l : } {M : Type u_1} [] [] (c₁ : l.Germ M) (c₂ : l.Germ M) (f : l.Germ β) :
c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)
theorem Filter.Germ.instAddAction'.proof_1 {α : Type u_2} {β : Type u_1} {l : } {M : Type u_3} [] [] (f : l.Germ β) :
0 +ᵥ f = f
instance Filter.Germ.instAddAction' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [] [] :
Equations
instance Filter.Germ.instMulAction' {α : Type u_1} {β : Type u_2} {l : } {M : Type u_5} [] [] :
MulAction (l.Germ M) (l.Germ β)
Equations
• Filter.Germ.instMulAction' =
instance Filter.Germ.instDistribMulAction {α : Type u_1} {l : } {M : Type u_5} {N : Type u_6} [] [] [] :
DistribMulAction M (l.Germ N)
Equations
• Filter.Germ.instDistribMulAction =
instance Filter.Germ.instDistribMulAction' {α : Type u_1} {l : } {M : Type u_5} {N : Type u_6} [] [] [] :
DistribMulAction (l.Germ M) (l.Germ N)
Equations
• Filter.Germ.instDistribMulAction' =
instance Filter.Germ.instModule {α : Type u_1} {l : } {M : Type u_5} {R : Type u_7} [] [] [Module R M] :
Module R (l.Germ M)
Equations
• Filter.Germ.instModule =
instance Filter.Germ.instModule' {α : Type u_1} {l : } {M : Type u_5} {R : Type u_7} [] [] [Module R M] :
Module (l.Germ R) (l.Germ M)
Equations
• Filter.Germ.instModule' =
instance Filter.Germ.instLE {α : Type u_1} {β : Type u_2} {l : } [LE β] :
LE (l.Germ β)
Equations
theorem Filter.Germ.le_def {α : Type u_1} {β : Type u_2} {l : } [LE β] :
(fun (x x_1 : l.Germ β) => x x_1) = Filter.Germ.LiftRel fun (x x_1 : β) => x x_1
@[simp]
theorem Filter.Germ.coe_le {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g : αβ} [LE β] :
f g f ≤ᶠ[l] g
theorem Filter.Germ.coe_nonneg {α : Type u_1} {β : Type u_2} {l : } [LE β] [Zero β] {f : αβ} :
0 f ∀ᶠ (x : α) in l, 0 f x
theorem Filter.Germ.const_le {α : Type u_1} {β : Type u_2} {l : } [LE β] {x : β} {y : β} :
x yx y
@[simp]
theorem Filter.Germ.const_le_iff {α : Type u_1} {β : Type u_2} {l : } [LE β] [l.NeBot] {x : β} {y : β} :
x y x y
instance Filter.Germ.instPreorder {α : Type u_1} {β : Type u_2} {l : } [] :
Preorder (l.Germ β)
Equations
instance Filter.Germ.instPartialOrder {α : Type u_1} {β : Type u_2} {l : } [] :
PartialOrder (l.Germ β)
Equations
• Filter.Germ.instPartialOrder =
instance Filter.Germ.instBot {α : Type u_1} {β : Type u_2} {l : } [Bot β] :
Bot (l.Germ β)
Equations
• Filter.Germ.instBot = { bot := }
instance Filter.Germ.instTop {α : Type u_1} {β : Type u_2} {l : } [Top β] :
Top (l.Germ β)
Equations
• Filter.Germ.instTop = { top := }
@[simp]
theorem Filter.Germ.const_bot {α : Type u_1} {β : Type u_2} {l : } [Bot β] :
=
@[simp]
theorem Filter.Germ.const_top {α : Type u_1} {β : Type u_2} {l : } [Top β] :
=
instance Filter.Germ.instOrderBot {α : Type u_1} {β : Type u_2} {l : } [LE β] [] :
OrderBot (l.Germ β)
Equations
• Filter.Germ.instOrderBot =
instance Filter.Germ.instOrderTop {α : Type u_1} {β : Type u_2} {l : } [LE β] [] :
OrderTop (l.Germ β)
Equations
• Filter.Germ.instOrderTop =
instance Filter.Germ.instBoundedOrder {α : Type u_1} {β : Type u_2} {l : } [LE β] [] :
BoundedOrder (l.Germ β)
Equations
• Filter.Germ.instBoundedOrder = let __spread.0 := Filter.Germ.instOrderBot; let __spread.1 := Filter.Germ.instOrderTop; BoundedOrder.mk
instance Filter.Germ.instSup {α : Type u_1} {β : Type u_2} {l : } [Sup β] :
Sup (l.Germ β)
Equations
instance Filter.Germ.instInf {α : Type u_1} {β : Type u_2} {l : } [Inf β] :
Inf (l.Germ β)
Equations
@[simp]
theorem Filter.Germ.const_sup {α : Type u_1} {β : Type u_2} {l : } [Sup β] (a : β) (b : β) :
(a b) = a b
@[simp]
theorem Filter.Germ.const_inf {α : Type u_1} {β : Type u_2} {l : } [Inf β] (a : β) (b : β) :
(a b) = a b
instance Filter.Germ.instSemilatticeSup {α : Type u_1} {β : Type u_2} {l : } [] :
SemilatticeSup (l.Germ β)
Equations
• Filter.Germ.instSemilatticeSup =
instance Filter.Germ.instSemilatticeInf {α : Type u_1} {β : Type u_2} {l : } [] :
SemilatticeInf (l.Germ β)
Equations
• Filter.Germ.instSemilatticeInf =
instance Filter.Germ.instLattice {α : Type u_1} {β : Type u_2} {l : } [] :
Lattice (l.Germ β)
Equations
• Filter.Germ.instLattice = let __spread.0 := Filter.Germ.instSemilatticeSup; let __spread.1 := Filter.Germ.instSemilatticeInf; Lattice.mk
instance Filter.Germ.instDistribLattice {α : Type u_1} {β : Type u_2} {l : } [] :
DistribLattice (l.Germ β)
Equations
• Filter.Germ.instDistribLattice =
instance Filter.Germ.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} {l : } :
Equations
theorem Filter.Germ.instOrderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : } (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 : } :
OrderedCommMonoid (l.Germ β)
Equations
• Filter.Germ.instOrderedCommMonoid =
theorem Filter.Germ.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : } (f : l.Germ β) (g : l.Germ β) (h : l.Germ β) :
f + g f + hg h
instance Filter.Germ.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} {l : } :
Equations
instance Filter.Germ.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} {l : } :
Equations
• Filter.Germ.instOrderedCancelCommMonoid =
theorem Filter.Germ.instOrderedAddCommGroup.proof_5 {α : Type u_2} {β : Type u_1} {l : } (a : l.Germ β) :
-a + a = 0
theorem Filter.Germ.instOrderedAddCommGroup.proof_7 {α : Type u_2} {β : Type u_1} {l : } (a : l.Germ β) (b : l.Germ β) :
a b∀ (c : l.Germ β), c + a c + b
theorem Filter.Germ.instOrderedAddCommGroup.proof_6 {α : Type u_2} {β : Type u_1} {l : } (a : l.Germ β) (b : l.Germ β) :
a + b = b + a
theorem Filter.Germ.instOrderedAddCommGroup.proof_4 {α : Type u_2} {β : Type u_1} {l : } (n : ) (a : l.Germ β) :
= -SubNegMonoid.zsmul (n.succ) a
theorem Filter.Germ.instOrderedAddCommGroup.proof_1 {α : Type u_2} {β : Type u_1} {l : } (a : l.Germ β) (b : l.Germ β) :
a - b = a + -b
theorem Filter.Germ.instOrderedAddCommGroup.proof_2 {α : Type u_2} {β : Type u_1} {l : } (a : l.Germ β) :
= 0
theorem Filter.Germ.instOrderedAddCommGroup.proof_3 {α : Type u_2} {β : Type u_1} {l : } (n : ) (a : l.Germ β) :
instance Filter.Germ.instOrderedAddCommGroup {α : Type u_1} {β : Type u_2} {l : } :
Equations
instance Filter.Germ.instOrderedCommGroup {α : Type u_1} {β : Type u_2} {l : } [] :
OrderedCommGroup (l.Germ β)
Equations
instance Filter.Germ.instExistsAddOfLE {α : Type u_1} {β : Type u_2} {l : } [Add β] [LE β] [] :
Equations
• =
instance Filter.Germ.instExistsMulOfLE {α : Type u_1} {β : Type u_2} {l : } [Mul β] [LE β] [] :
ExistsMulOfLE (l.Germ β)
Equations
• =
theorem Filter.Germ.instCanonicallyOrderedAddCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} {l : } (x : l.Germ β) (y : l.Germ β) :
x x + y
Equations
theorem Filter.Germ.instCanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} {l : } :
∀ {a b : l.Germ β}, a b∃ (c : l.Germ β), b = a + c
instance Filter.Germ.instCanonicallyOrderedCommMonoid {α : Type u_1} {β : Type u_2} {l : } :
Equations
• Filter.Germ.instCanonicallyOrderedCommMonoid = let __spread.0 := ;
instance Filter.Germ.instOrderedSemiring {α : Type u_1} {β : Type u_2} {l : } [] :
OrderedSemiring (l.Germ β)
Equations