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;

Tags

filter, germ

theorem Filter.const_eventuallyEq' {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {a : β} {b : β} : (∀ᶠ (x : α) in l, a = b) ↔ a = b

theorem Filter.const_eventuallyEq {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {a : β} {b : β} : ((fun (x : α) => a) =ᶠ[l] fun (x : α) => b) ↔ a = b

def Filter.germSetoid {α : Type u_1} (l : Filter α) (β : Type u_5) : Setoid (α → β)

Setoid used to define the space of germs.

Equations

• l.germSetoid β = { r := l.EventuallyEq, iseqv := ⋯ }

def Filter.Germ {α : Type u_1} (l : Filter α) (β : Type u_5) : Type (max u_1 u_5)

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

Equations

• l.Germ β = Quotient (l.germSetoid β)

def Filter.productSetoid {α : Type u_1} (l : Filter α) (ε : α → 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 := ⋯ }

def Filter.Product {α : Type u_1} (l : Filter α) (ε : α → 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

• l.Product ε = Quotient (l.productSetoid ε)

instance Filter.Product.coeTC {α : Type u_1} {l : Filter α} {ε : α → Type u_5} : CoeTC ((a : α) → ε a) (l.Product ε)

Equations

• Filter.Product.coeTC = { coe := Quotient.mk' }

instance Filter.Product.instInhabited {α : Type u_1} {l : Filter α} {ε : α → 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 : Filter α} : (α → β) → l.Germ β

Equations

• Filter.Germ.ofFun = Quotient.mk'

instance Filter.Germ.instCoeTCForall {α : Type u_1} {β : Type u_2} {l : Filter α} : CoeTC (α → β) (l.Germ β)

Equations

• Filter.Germ.instCoeTCForall = { coe := Filter.Germ.ofFun }

def Filter.Germ.const {α : Type u_1} {β : Type u_2} {l : Filter α} (b : β) : l.Germ β

Equations

• ↑b = ↑fun (x : α) => b

instance Filter.Germ.coeTC {α : Type u_1} {β : Type u_2} {l : Filter α} : CoeTC β (l.Germ β)

Equations

• Filter.Germ.coeTC = { coe := Filter.Germ.const }

def Filter.Germ.IsConstant {α : Type u_1} {β : Type u_2} {l : Filter α} (P : l.Germ β) : Prop

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

Equations

• P.IsConstant = Quotient.liftOn P (fun (f : α → β) => ∃ (b : β), f =ᶠ[l] fun (x : α) => b) ⋯

theorem Filter.Germ.isConstant_coe {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} {b : β} (h : ∀ (x' : α), f x' = b) : (↑f).IsConstant

@[simp]

theorem Filter.Germ.isConstant_coe_const {α : Type u_1} {β : Type u_2} {l : Filter α} {b : β} : (↑fun (x : α) => b).IsConstant

theorem Filter.Germ.isConstant_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {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 : Filter α) (f : α → β) : Quot.mk Setoid.r f = ↑f

@[simp]

theorem Filter.Germ.mk'_eq_coe {α : Type u_1} {β : Type u_2} (l : Filter α) (f : α → β) : Quotient.mk' f = ↑f

theorem Filter.Germ.inductionOn {α : Type u_1} {β : Type u_2} {l : Filter α} (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 : Filter α} (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 : Filter α} (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 : Filter α} {lc : Filter γ} (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

• Filter.Germ.map' F hF = Quotient.map' F hF

def Filter.Germ.liftOn {α : Type u_1} {β : Type u_2} {l : Filter α} {γ : Sort u_5} (f : l.Germ β) (F : (α → β) → γ) (hF : (l.EventuallyEq ⇒ fun (x1 x2 : γ) => x1 = x2) 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

• f.liftOn F hF = Quotient.liftOn' f F hF

@[simp]

theorem Filter.Germ.map'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (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 : Filter α} {f : α → β} {g : α → β} : ↑f = ↑g ↔ f =ᶠ[l] g

theorem Filter.EventuallyEq.germ_eq {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {g : α → β} : f =ᶠ[l] g → ↑f = ↑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 : Filter α} (op : β → γ) : l.Germ β → l.Germ γ

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

Equations

• Filter.Germ.map op = Filter.Germ.map' (fun (x : α → β) => op ∘ x) ⋯

@[simp]

theorem Filter.Germ.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (op : β → γ) (f : α → β) : Filter.Germ.map op ↑f = ↑(op ∘ f)

@[simp]

theorem Filter.Germ.map_id {α : Type u_1} {β : Type u_2} {l : Filter α} : Filter.Germ.map id = id

theorem Filter.Germ.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (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 : Filter α} (op : β → γ → δ) : l.Germ β → l.Germ γ → l.Germ δ

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

Equations

• Filter.Germ.map₂ op = Quotient.map₂' (fun (f : α → β) (g : α → γ) (x : α) => op (f x) (g x)) ⋯

@[simp]

theorem Filter.Germ.map₂_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (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 : Filter α} (f : l.Germ β) (lb : Filter β) : Prop

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

• f.Tendsto lb = f.liftOn (fun (f : α → β) => Filter.Tendsto f l lb) ⋯

@[simp]

theorem Filter.Germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β} : (↑f).Tendsto lb ↔ Filter.Tendsto f l lb

theorem Filter.Tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β} : 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 : Filter α} (f : l.Germ β) {lc : Filter γ} (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 : α → β) => Filter.Germ.map f g) ⋯

@[simp]

theorem Filter.Germ.coe_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : α → β) {lc : Filter γ} {g : lc.Germ α} (hg : g.Tendsto l) : (↑f).compTendsto' g hg = Filter.Germ.map f g

def Filter.Germ.compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : l.Germ β) {lc : Filter γ} (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 ⋯

@[simp]

theorem Filter.Germ.coe_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : α → β) {lc : Filter γ} {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 : Filter α} (f : l.Germ β) {lc : Filter γ} {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 : Filter α} {l' : Filter β} (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 : Filter α} {f : α → β} {lc : Filter γ} {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 : Filter α} {f : l.Germ β} {lc : Filter γ} {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 : Filter α} [l.NeBot] {a : β} {b : β} : ↑a = ↑b ↔ a = b

@[simp]

theorem Filter.Germ.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter α) (a : β) (f : β → γ) : Filter.Germ.map f ↑a = ↑(f a)

@[simp]

theorem Filter.Germ.map₂_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : Filter α) (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 : Filter α} (b : β) {lc : Filter γ} {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 : Filter α} (b : β) {lc : Filter γ} {g : lc.Germ α} (hg : g.Tendsto l) : (↑b).compTendsto' g hg = ↑b

def Filter.Germ.LiftPred {α : Type u_1} {β : Type u_2} {l : Filter α} (p : β → Prop) (f : l.Germ β) : Prop

Lift a predicate on β to Germ l β.

Equations

• Filter.Germ.LiftPred p f = f.liftOn (fun (f : α → β) => ∀ᶠ (x : α) in l, p (f x)) ⋯

@[simp]

theorem Filter.Germ.liftPred_coe {α : Type u_1} {β : Type u_2} {l : Filter α} {p : β → Prop} {f : α → β} : Filter.Germ.LiftPred p ↑f ↔ ∀ᶠ (x : α) in l, p (f x)

theorem Filter.Germ.liftPred_const {α : Type u_1} {β : Type u_2} {l : Filter α} {p : β → Prop} {x : β} (hx : p x) : Filter.Germ.LiftPred p ↑x

@[simp]

theorem Filter.Germ.liftPred_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {p : β → Prop} {x : β} : Filter.Germ.LiftPred p ↑x ↔ p x

def Filter.Germ.LiftRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (r : β → γ → Prop) (f : l.Germ β) (g : l.Germ γ) : Prop

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

Equations

• Filter.Germ.LiftRel r f g = Quotient.liftOn₂' f g (fun (f : α → β) (g : α → γ) => ∀ᶠ (x : α) in l, r (f x) (g x)) ⋯

@[simp]

theorem Filter.Germ.liftRel_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {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 : Filter α} {r : β → γ → Prop} {x : β} {y : γ} (h : r x y) : Filter.Germ.LiftRel r ↑x ↑y

@[simp]

theorem Filter.Germ.liftRel_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} [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 : Filter α} [Inhabited β] : Inhabited (l.Germ β)

Equations

• Filter.Germ.instInhabited = { default := ↑default }

instance Filter.Germ.instAdd {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] : Add (l.Germ M)

Equations

• Filter.Germ.instAdd = { add := Filter.Germ.map₂ fun (x1 x2 : M) => x1 + x2 }

instance Filter.Germ.instMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] : Mul (l.Germ M)

Equations

• Filter.Germ.instMul = { mul := Filter.Germ.map₂ fun (x1 x2 : M) => x1 * x2 }

@[simp]

theorem Filter.Germ.coe_add {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] (f : α → M) (g : α → M) : ↑(f + g) = ↑f + ↑g

@[simp]

theorem Filter.Germ.coe_mul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] (f : α → M) (g : α → M) : ↑(f * g) = ↑f * ↑g

instance Filter.Germ.instZero {α : Type u_1} {l : Filter α} {M : Type u_5} [Zero M] : Zero (l.Germ M)

Equations

• Filter.Germ.instZero = { zero := ↑0 }

instance Filter.Germ.instOne {α : Type u_1} {l : Filter α} {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 : Filter α} {M : Type u_5} [Zero M] : ↑0 = 0

@[simp]

theorem Filter.Germ.coe_one {α : Type u_1} {l : Filter α} {M : Type u_5} [One M] : ↑1 = 1

instance Filter.Germ.instAddSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [AddSemigroup M] : AddSemigroup (l.Germ M)

Equations

• Filter.Germ.instAddSemigroup = AddSemigroup.mk ⋯

theorem Filter.Germ.instAddSemigroup.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddSemigroup M] (a : l.Germ M) (b : l.Germ M) (c : l.Germ M) : a + b + c = a + (b + c)

instance Filter.Germ.instSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [Semigroup M] : Semigroup (l.Germ M)

Equations

• Filter.Germ.instSemigroup = Semigroup.mk ⋯

theorem Filter.Germ.instAddCommSemigroup.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddCommSemigroup M] (q₁ : Quotient (l.germSetoid M)) (q₂ : Quotient (l.germSetoid M)) : q₁ + q₂ = q₂ + q₁

instance Filter.Germ.instAddCommSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [AddCommSemigroup M] : AddCommSemigroup (l.Germ M)

Equations

• Filter.Germ.instAddCommSemigroup = AddCommSemigroup.mk ⋯

instance Filter.Germ.instCommSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [CommSemigroup M] : CommSemigroup (l.Germ M)

Equations

• Filter.Germ.instCommSemigroup = CommSemigroup.mk ⋯

instance Filter.Germ.instIsAddLeftCancel {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] [IsLeftCancelAdd M] : IsLeftCancelAdd (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instIsLeftCancelMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] [IsLeftCancelMul M] : IsLeftCancelMul (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instIsAddRightCancel {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] [IsRightCancelAdd M] : IsRightCancelAdd (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instIsRightCancelMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] [IsRightCancelMul M] : IsRightCancelMul (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instIsAddCancel {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] [IsCancelAdd M] : IsCancelAdd (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instIsCancelMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] [IsCancelMul M] : IsCancelMul (l.Germ M)

Equations

• ⋯ = ⋯

instance Filter.Germ.instAddLeftCancelSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [AddLeftCancelSemigroup M] : AddLeftCancelSemigroup (l.Germ M)

Equations

• Filter.Germ.instAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

theorem Filter.Germ.instAddLeftCancelSemigroup.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddLeftCancelSemigroup M] : ∀ (x x_1 x_2 : l.Germ M), x + x_1 = x + x_2 → x_1 = x_2

instance Filter.Germ.instLeftCancelSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [LeftCancelSemigroup M] : LeftCancelSemigroup (l.Germ M)

Equations

• Filter.Germ.instLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯

instance Filter.Germ.instAddRightCancelSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [AddRightCancelSemigroup M] : AddRightCancelSemigroup (l.Germ M)

Equations

• Filter.Germ.instAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

theorem Filter.Germ.instAddRightCancelSemigroup.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddRightCancelSemigroup M] : ∀ (x x_1 x_2 : l.Germ M), x + x_1 = x_2 + x_1 → x = x_2

instance Filter.Germ.instRightCancelSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [RightCancelSemigroup M] : RightCancelSemigroup (l.Germ M)

Equations

• Filter.Germ.instRightCancelSemigroup = RightCancelSemigroup.mk ⋯

theorem Filter.Germ.instAddZeroClass.proof_2 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddZeroClass M] (q : Quotient (l.germSetoid M)) : q + 0 = q

instance Filter.Germ.instAddZeroClass {α : Type u_1} {l : Filter α} {M : Type u_5} [AddZeroClass M] : AddZeroClass (l.Germ M)

Equations

• Filter.Germ.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

theorem Filter.Germ.instAddZeroClass.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddZeroClass M] (q : Quotient (l.germSetoid M)) : 0 + q = q

instance Filter.Germ.instMulOneClass {α : Type u_1} {l : Filter α} {M : Type u_5} [MulOneClass M] : MulOneClass (l.Germ M)

Equations

• Filter.Germ.instMulOneClass = MulOneClass.mk ⋯ ⋯

instance Filter.Germ.instVAdd {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [VAdd M G] : VAdd M (l.Germ G)

Equations

• Filter.Germ.instVAdd = { vadd := fun (n : M) => Filter.Germ.map fun (x : G) => n +ᵥ x }

instance Filter.Germ.instSMul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] : SMul M (l.Germ G)

Equations

• Filter.Germ.instSMul = { smul := fun (n : M) => Filter.Germ.map fun (x : G) => n • x }

instance Filter.Germ.instPow {α : Type u_1} {l : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {M : Type u_5} {G : Type u_6} [Pow G M] (a : G) (n : M) : ↑(a ^ n) = ↑a ^ n

theorem Filter.Germ.instAddMonoid.proof_7 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] (x : l.Germ M) : AddMonoid.nsmul 0 x = 0

theorem Filter.Germ.instAddMonoid.proof_6 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] (a : l.Germ M) : a + 0 = a

instance Filter.Germ.instAddMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoid M] : AddMonoid (l.Germ M)

Equations

• Filter.Germ.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : l.Germ M) => n • a) ⋯ ⋯

theorem Filter.Germ.instAddMonoid.proof_2 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] : ↑0 = ↑0

theorem Filter.Germ.instAddMonoid.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} : Function.Surjective (Quot.mk Setoid.r)

theorem Filter.Germ.instAddMonoid.proof_8 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] (n : ℕ) (x : l.Germ M) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

theorem Filter.Germ.instAddMonoid.proof_4 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] : ∀ (x : α → M) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem Filter.Germ.instAddMonoid.proof_3 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] : ∀ (x x_1 : α → M), ↑(x + x_1) = ↑(x + x_1)

theorem Filter.Germ.instAddMonoid.proof_5 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] (a : l.Germ M) : 0 + a = a

instance Filter.Germ.instMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [Monoid M] : Monoid (l.Germ M)

Equations

• Filter.Germ.instMonoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : l.Germ M) => a ^ n) ⋯ ⋯

theorem Filter.Germ.coeAddHom.proof_2 {α : Type u_1} {M : Type u_2} [AddMonoid M] (l : Filter α) : ∀ (x x_1 : α → M), { toFun := Filter.Germ.ofFun, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := Filter.Germ.ofFun, map_zero' := ⋯ }.toFun (x + x_1)

theorem Filter.Germ.coeAddHom.proof_1 {α : Type u_1} {M : Type u_2} [AddMonoid M] (l : Filter α) : ↑0 = ↑0

def Filter.Germ.coeAddHom {α : Type u_1} {M : Type u_5} [AddMonoid M] (l : Filter α) : (α → M) →+ l.Germ M

Coercion from functions to germs as an additive monoid homomorphism.

Equations

• Filter.Germ.coeAddHom l = { toFun := Filter.Germ.ofFun, map_zero' := ⋯, map_add' := ⋯ }

def Filter.Germ.coeMulHom {α : Type u_1} {M : Type u_5} [Monoid M] (l : Filter α) : (α → M) →* l.Germ M

Coercion from functions to germs as a monoid homomorphism.

Equations

• Filter.Germ.coeMulHom l = { toFun := Filter.Germ.ofFun, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Filter.Germ.coe_coeAddHom {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoid M] : ⇑(Filter.Germ.coeAddHom l) = Filter.Germ.ofFun

@[simp]

theorem Filter.Germ.coe_coeMulHom {α : Type u_1} {l : Filter α} {M : Type u_5} [Monoid M] : ⇑(Filter.Germ.coeMulHom l) = Filter.Germ.ofFun

instance Filter.Germ.instAddCommMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [AddCommMonoid M] : AddCommMonoid (l.Germ M)

Equations

• Filter.Germ.instAddCommMonoid = AddCommMonoid.mk ⋯

theorem Filter.Germ.instAddCommMonoid.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddCommMonoid M] (a : l.Germ M) (b : l.Germ M) : a + b = b + a

instance Filter.Germ.instCommMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [CommMonoid M] : CommMonoid (l.Germ M)

Equations

• Filter.Germ.instCommMonoid = CommMonoid.mk ⋯

instance Filter.Germ.instNatCast {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] : NatCast (l.Germ M)

Equations

• Filter.Germ.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

@[simp]

theorem Filter.Germ.natCast_def {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ℕ) : (↑fun (x : α) => ↑n) = ↑n

@[simp]

theorem Filter.Germ.const_nat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Filter.Germ.coe_ofNat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Filter.Germ.const_ofNat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

instance Filter.Germ.instIntCast {α : Type u_1} {l : Filter α} {M : Type u_5} [IntCast M] : IntCast (l.Germ M)

Equations

• Filter.Germ.instIntCast = { intCast := fun (n : ℤ) => ↑↑n }

@[simp]

theorem Filter.Germ.intCast_def {α : Type u_1} {l : Filter α} {M : Type u_5} [IntCast M] (n : ℤ) : (↑fun (x : α) => ↑n) = ↑n

@[deprecated Filter.Germ.natCast_def]

theorem Filter.Germ.coe_nat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (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 : Filter α} {M : Type u_5} [IntCast M] (n : ℤ) : (↑fun (x : α) => ↑n) = ↑n

Alias of Filter.Germ.intCast_def.

instance Filter.Germ.instAddMonoidWithOne {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoidWithOne M] : AddMonoidWithOne (l.Germ M)

Equations

• Filter.Germ.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

instance Filter.Germ.instAddCommMonoidWithOne {α : Type u_1} {l : Filter α} {M : Type u_5} [AddCommMonoidWithOne M] : AddCommMonoidWithOne (l.Germ M)

Equations

• Filter.Germ.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

instance Filter.Germ.instNeg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] : Neg (l.Germ G)

Equations

• Filter.Germ.instNeg = { neg := Filter.Germ.map Neg.neg }

instance Filter.Germ.instInv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] : Inv (l.Germ G)

Equations

• Filter.Germ.instInv = { inv := Filter.Germ.map Inv.inv }

@[simp]

theorem Filter.Germ.coe_neg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] (f : α → G) : ↑(-f) = -↑f

@[simp]

theorem Filter.Germ.coe_inv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] (f : α → G) : ↑f⁻¹ = (↑f)⁻¹

@[simp]

theorem Filter.Germ.const_neg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] (a : G) : ↑(-a) = -↑a

@[simp]

theorem Filter.Germ.const_inv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] (a : G) : ↑a⁻¹ = (↑a)⁻¹

instance Filter.Germ.instSub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] : Sub (l.Germ M)

Equations

• Filter.Germ.instSub = { sub := Filter.Germ.map₂ fun (x1 x2 : M) => x1 - x2 }

instance Filter.Germ.instDiv {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] : Div (l.Germ M)

Equations

• Filter.Germ.instDiv = { div := Filter.Germ.map₂ fun (x1 x2 : M) => x1 / x2 }

@[simp]

theorem Filter.Germ.coe_sub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] (f : α → M) (g : α → M) : ↑(f - g) = ↑f - ↑g

@[simp]

theorem Filter.Germ.coe_div {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] (f : α → M) (g : α → M) : ↑(f / g) = ↑f / ↑g

@[simp]

theorem Filter.Germ.const_sub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] (a : M) (b : M) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem Filter.Germ.const_div {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] (a : M) (b : M) : ↑(a / b) = ↑a / ↑b

theorem Filter.Germ.instInvolutiveNeg.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [InvolutiveNeg G] (q : Quotient (l.germSetoid G)) : - -q = q

instance Filter.Germ.instInvolutiveNeg {α : Type u_1} {l : Filter α} {G : Type u_6} [InvolutiveNeg G] : InvolutiveNeg (l.Germ G)

Equations

• Filter.Germ.instInvolutiveNeg = InvolutiveNeg.mk ⋯

instance Filter.Germ.instInvolutiveInv {α : Type u_1} {l : Filter α} {G : Type u_6} [InvolutiveInv G] : InvolutiveInv (l.Germ G)

Equations

• Filter.Germ.instInvolutiveInv = InvolutiveInv.mk ⋯

instance Filter.Germ.instHasDistribNeg {α : Type u_1} {l : Filter α} {G : Type u_6} [Mul G] [HasDistribNeg G] : HasDistribNeg (l.Germ G)

Equations

• Filter.Germ.instHasDistribNeg = HasDistribNeg.mk ⋯ ⋯

theorem Filter.Germ.instNegZeroClass.proof_1 {α : Type u_2} {l : Filter α} {G : Type u_1} [NegZeroClass G] : ↑((fun (x : α → G) => Neg.neg ∘ x) fun (x : α) => 0) = ↑fun (x : α) => 0

instance Filter.Germ.instNegZeroClass {α : Type u_1} {l : Filter α} {G : Type u_6} [NegZeroClass G] : NegZeroClass (l.Germ G)

Equations

• Filter.Germ.instNegZeroClass = NegZeroClass.mk ⋯

instance Filter.Germ.instInvOneClass {α : Type u_1} {l : Filter α} {G : Type u_6} [InvOneClass G] : InvOneClass (l.Germ G)

Equations

• Filter.Germ.instInvOneClass = InvOneClass.mk ⋯

instance Filter.Germ.subNegMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [SubNegMonoid G] : SubNegMonoid (l.Germ G)

Equations

• Filter.Germ.subNegMonoid = SubNegMonoid.mk ⋯ (fun (z : ℤ) (f : l.Germ G) => z • f) ⋯ ⋯ ⋯

theorem Filter.Germ.subNegMonoid.proof_2 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] (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 : Filter α} {G : Type u_2} [SubNegMonoid G] (q₁ : Quotient (l.germSetoid G)) (q₂ : Quotient (l.germSetoid G)) : q₁ - q₂ = q₁ + -q₂

theorem Filter.Germ.subNegMonoid.proof_4 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] : ∀ (x : ℕ) (q : Quotient (l.germSetoid G)), (fun (z : ℤ) (f : l.Germ G) => z • f) (Int.negSucc x) q = -(fun (z : ℤ) (f : l.Germ G) => z • f) (↑x.succ) q

theorem Filter.Germ.subNegMonoid.proof_3 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] : ∀ (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) (Int.ofNat x) q + q

instance Filter.Germ.instDivInvMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [DivInvMonoid G] : DivInvMonoid (l.Germ G)

Equations

• Filter.Germ.instDivInvMonoid = DivInvMonoid.mk ⋯ (fun (z : ℤ) (f : l.Germ G) => f ^ z) ⋯ ⋯ ⋯

instance Filter.Germ.instSubtractionMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [SubtractionMonoid G] : SubtractionMonoid (l.Germ G)

Equations

• Filter.Germ.instSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

theorem Filter.Germ.instSubtractionMonoid.proof_2 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubtractionMonoid G] (x : l.Germ G) (y : l.Germ G) : -(x + y) = -y + -x

theorem Filter.Germ.instSubtractionMonoid.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubtractionMonoid G] (a : l.Germ G) : - -a = a

theorem Filter.Germ.instSubtractionMonoid.proof_3 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubtractionMonoid G] (x : l.Germ G) (y : l.Germ G) : x + y = 0 → -x = y

instance Filter.Germ.instDivisionMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [DivisionMonoid G] : DivisionMonoid (l.Germ G)

Equations

• Filter.Germ.instDivisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

instance Filter.Germ.instAddGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [AddGroup G] : AddGroup (l.Germ G)

Equations

• Filter.Germ.instAddGroup = AddGroup.mk ⋯

theorem Filter.Germ.instAddGroup.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [AddGroup G] (q : Quotient (l.germSetoid G)) : -q + q = 0

instance Filter.Germ.instGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [Group G] : Group (l.Germ G)

Equations

• Filter.Germ.instGroup = Group.mk ⋯

theorem Filter.Germ.instAddCommGroup.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [AddCommGroup G] (a : l.Germ G) (b : l.Germ G) : a + b = b + a

instance Filter.Germ.instAddCommGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [AddCommGroup G] : AddCommGroup (l.Germ G)

Equations

• Filter.Germ.instAddCommGroup = AddCommGroup.mk ⋯

instance Filter.Germ.instCommGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [CommGroup G] : CommGroup (l.Germ G)

Equations

• Filter.Germ.instCommGroup = CommGroup.mk ⋯

instance Filter.Germ.instAddGroupWithOne {α : Type u_1} {l : Filter α} {G : Type u_6} [AddGroupWithOne G] : AddGroupWithOne (l.Germ G)

Equations

• Filter.Germ.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instNontrivial {α : Type u_1} {l : Filter α} {R : Type u_5} [Nontrivial R] [l.NeBot] : Nontrivial (l.Germ R)

Equations

• ⋯ = ⋯

instance Filter.Germ.instMulZeroClass {α : Type u_1} {l : Filter α} {R : Type u_5} [MulZeroClass R] : MulZeroClass (l.Germ R)

Equations

• Filter.Germ.instMulZeroClass = MulZeroClass.mk ⋯ ⋯

instance Filter.Germ.instMulZeroOneClass {α : Type u_1} {l : Filter α} {R : Type u_5} [MulZeroOneClass R] : MulZeroOneClass (l.Germ R)

Equations

• Filter.Germ.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯

instance Filter.Germ.instMonoidWithZero {α : Type u_1} {l : Filter α} {R : Type u_5} [MonoidWithZero R] : MonoidWithZero (l.Germ R)

Equations

• Filter.Germ.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

instance Filter.Germ.instDistrib {α : Type u_1} {l : Filter α} {R : Type u_5} [Distrib R] : Distrib (l.Germ R)

Equations

• Filter.Germ.instDistrib = Distrib.mk ⋯ ⋯

instance Filter.Germ.instNonUnitalNonAssocSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (l.Germ R)

Equations

• Filter.Germ.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instNonUnitalSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalSemiring R] : NonUnitalSemiring (l.Germ R)

Equations

• Filter.Germ.instNonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance Filter.Germ.instNonAssocSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [NonAssocSemiring R] : NonAssocSemiring (l.Germ R)

Equations

• Filter.Germ.instNonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instNonUnitalNonAssocRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (l.Germ R)

Equations

• Filter.Germ.instNonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instNonUnitalRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalRing R] : NonUnitalRing (l.Germ R)

Equations

• Filter.Germ.instNonUnitalRing = NonUnitalRing.mk ⋯

instance Filter.Germ.instNonAssocRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonAssocRing R] : NonAssocRing (l.Germ R)

Equations

• Filter.Germ.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [Semiring R] : Semiring (l.Germ R)

Equations

• Filter.Germ.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

instance Filter.Germ.instRing {α : Type u_1} {l : Filter α} {R : Type u_5} [Ring R] : Ring (l.Germ R)

Equations

• Filter.Germ.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instNonUnitalCommSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalCommSemiring R] : NonUnitalCommSemiring (l.Germ R)

Equations

• Filter.Germ.instNonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance Filter.Germ.instCommSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [CommSemiring R] : CommSemiring (l.Germ R)

Equations

• Filter.Germ.instCommSemiring = CommSemiring.mk ⋯

instance Filter.Germ.instNonUnitalCommRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalCommRing R] : NonUnitalCommRing (l.Germ R)

Equations

• Filter.Germ.instNonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance Filter.Germ.instCommRing {α : Type u_1} {l : Filter α} {R : Type u_5} [CommRing R] : CommRing (l.Germ R)

Equations

• Filter.Germ.instCommRing = CommRing.mk ⋯

def Filter.Germ.coeRingHom {α : Type u_1} {R : Type u_5} [Semiring R] (l : Filter α) : (α → R) →+* l.Germ R

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

Equations

• Filter.Germ.coeRingHom l = { toFun := Filter.Germ.ofFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Filter.Germ.coe_coeRingHom {α : Type u_1} {l : Filter α} {R : Type u_5} [Semiring R] : ⇑(Filter.Germ.coeRingHom l) = Filter.Germ.ofFun

instance Filter.Germ.instVAdd' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [VAdd M β] : VAdd (l.Germ M) (l.Germ β)

Equations

• Filter.Germ.instVAdd' = { vadd := Filter.Germ.map₂ fun (x1 : M) (x2 : β) => x1 +ᵥ x2 }

instance Filter.Germ.instSMul' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [SMul M β] : SMul (l.Germ M) (l.Germ β)

Equations

• Filter.Germ.instSMul' = { smul := Filter.Germ.map₂ fun (x1 : M) (x2 : β) => x1 • x2 }

@[simp]

theorem Filter.Germ.coe_vadd' {α : Type u_1} {β : Type u_2} {l : Filter α} {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 : Filter α} {M : Type u_5} [SMul M β] (c : α → M) (f : α → β) : ↑(c • f) = ↑c • ↑f

theorem Filter.Germ.instAddAction.proof_2 {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (c₁ : M) (c₂ : M) (f : l.Germ β) : c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)

instance Filter.Germ.instAddAction {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [AddMonoid M] [AddAction M β] : AddAction M (l.Germ β)

Equations

• Filter.Germ.instAddAction = AddAction.mk ⋯ ⋯

theorem Filter.Germ.instAddAction.proof_1 {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (f : l.Germ β) : 0 +ᵥ f = f

instance Filter.Germ.instMulAction {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [Monoid M] [MulAction M β] : MulAction M (l.Germ β)

Equations

• Filter.Germ.instMulAction = MulAction.mk ⋯ ⋯

theorem Filter.Germ.instAddAction'.proof_2 {α : Type u_1} {β : Type u_3} {l : Filter α} {M : Type u_2} [AddMonoid M] [AddAction M β] (c₁ : l.Germ M) (c₂ : l.Germ M) (f : l.Germ β) : c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)

instance Filter.Germ.instAddAction' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [AddMonoid M] [AddAction M β] : AddAction (l.Germ M) (l.Germ β)

Equations

• Filter.Germ.instAddAction' = AddAction.mk ⋯ ⋯

theorem Filter.Germ.instAddAction'.proof_1 {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (f : l.Germ β) : 0 +ᵥ f = f

instance Filter.Germ.instMulAction' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [Monoid M] [MulAction M β] : MulAction (l.Germ M) (l.Germ β)

Equations

• Filter.Germ.instMulAction' = MulAction.mk ⋯ ⋯

instance Filter.Germ.instDistribMulAction {α : Type u_1} {l : Filter α} {M : Type u_5} {N : Type u_6} [Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction M (l.Germ N)

Equations

• Filter.Germ.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

instance Filter.Germ.instDistribMulAction' {α : Type u_1} {l : Filter α} {M : Type u_5} {N : Type u_6} [Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction (l.Germ M) (l.Germ N)

Equations

• Filter.Germ.instDistribMulAction' = DistribMulAction.mk ⋯ ⋯

instance Filter.Germ.instModule {α : Type u_1} {l : Filter α} {M : Type u_5} {R : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : Module R (l.Germ M)

Equations

• Filter.Germ.instModule = Module.mk ⋯ ⋯

instance Filter.Germ.instModule' {α : Type u_1} {l : Filter α} {M : Type u_5} {R : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : Module (l.Germ R) (l.Germ M)

Equations

• Filter.Germ.instModule' = Module.mk ⋯ ⋯

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

Equations

• Filter.Germ.instLE = { le := Filter.Germ.LiftRel fun (x1 x2 : β) => x1 ≤ x2 }

theorem Filter.Germ.le_def {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] : (fun (x1 x2 : l.Germ β) => x1 ≤ x2) = Filter.Germ.LiftRel fun (x1 x2 : β) => x1 ≤ x2

@[simp]

theorem Filter.Germ.coe_le {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {g : α → β} [LE β] : ↑f ≤ ↑g ↔ f ≤ᶠ[l] g

theorem Filter.Germ.coe_nonneg {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [Zero β] {f : α → β} : 0 ≤ ↑f ↔ ∀ᶠ (x : α) in l, 0 ≤ f x

theorem Filter.Germ.const_le {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] {x : β} {y : β} : x ≤ y → ↑x ≤ ↑y

@[simp]

theorem Filter.Germ.const_le_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [l.NeBot] {x : β} {y : β} : ↑x ≤ ↑y ↔ x ≤ y

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

Equations

• Filter.Germ.instPreorder = Preorder.mk ⋯ ⋯ ⋯

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

Equations

• Filter.Germ.instPartialOrder = PartialOrder.mk ⋯

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

Equations

• Filter.Germ.instBot = { bot := ↑⊥ }

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

Equations

• Filter.Germ.instTop = { top := ↑⊤ }

@[simp]

theorem Filter.Germ.const_bot {α : Type u_1} {β : Type u_2} {l : Filter α} [Bot β] : ↑⊥ = ⊥

@[simp]

theorem Filter.Germ.const_top {α : Type u_1} {β : Type u_2} {l : Filter α} [Top β] : ↑⊤ = ⊤

instance Filter.Germ.instOrderBot {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [OrderBot β] : OrderBot (l.Germ β)

Equations

• Filter.Germ.instOrderBot = OrderBot.mk ⋯

instance Filter.Germ.instOrderTop {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [OrderTop β] : OrderTop (l.Germ β)

Equations

• Filter.Germ.instOrderTop = OrderTop.mk ⋯

instance Filter.Germ.instBoundedOrder {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [BoundedOrder β] : BoundedOrder (l.Germ β)

Equations

• Filter.Germ.instBoundedOrder = BoundedOrder.mk

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

Equations

• Filter.Germ.instSup = { sup := Filter.Germ.map₂ fun (x1 x2 : β) => x1 ⊔ x2 }

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

Equations

• Filter.Germ.instInf = { inf := Filter.Germ.map₂ fun (x1 x2 : β) => x1 ⊓ x2 }

@[simp]

theorem Filter.Germ.const_sup {α : Type u_1} {β : Type u_2} {l : Filter α} [Sup β] (a : β) (b : β) : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem Filter.Germ.const_inf {α : Type u_1} {β : Type u_2} {l : Filter α} [Inf β] (a : β) (b : β) : ↑(a ⊓ b) = ↑a ⊓ ↑b

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

Equations

• Filter.Germ.instSemilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

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

Equations

• Filter.Germ.instSemilatticeInf = SemilatticeInf.mk ⋯ ⋯ ⋯

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

Equations

• Filter.Germ.instLattice = Lattice.mk ⋯ ⋯ ⋯

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

Equations

• Filter.Germ.instDistribLattice = DistribLattice.mk ⋯

instance Filter.Germ.instExistsAddOfLE {α : Type u_1} {β : Type u_2} {l : Filter α} [Add β] [LE β] [ExistsAddOfLE β] : ExistsAddOfLE (l.Germ β)

Equations

• ⋯ = ⋯

instance Filter.Germ.instExistsMulOfLE {α : Type u_1} {β : Type u_2} {l : Filter α} [Mul β] [LE β] [ExistsMulOfLE β] : ExistsMulOfLE (l.Germ β)

Equations

• ⋯ = ⋯