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

source

theorem Filter.const_eventuallyEq' {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :

(∀ᶠ (x : α) in l, a = b) ↔ a = b

source

theorem Filter.const_eventuallyEq {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :

((fun (x : α) => a) =ᶠ[l] fun (x : α) => b) ↔ a = b

source

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

Setoid (α → β)

Setoid used to define the space of germs.

Equations

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

source

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

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

Instances For

source

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

Filter.productSetoid l ε = { r := fun (f g : (a : α) → ε a) => ∀ᶠ (a : α) in l, f a = g a, iseqv := ⋯ }

source

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

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

Instances For

source

instance Filter.Product.coeTC {α : Type u_1} {l : Filter α} {ε : α → Type u_5} :

CoeTC ((a : α) → ε a) (Filter.Product l ε)

Equations

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

source

instance Filter.Product.inhabited {α : Type u_1} {l : Filter α} {ε : α → Type u_5} [(a : α) → Inhabited (ε a)] :

Inhabited (Filter.Product l ε)

Equations

Filter.Product.inhabited = { default := Quotient.mk' fun (a : α) => default }

source

def Filter.Germ.ofFun {α : Type u_1} {β : Type u_2} {l : Filter α} :

(α → β) → Filter.Germ l β

Equations

Filter.Germ.ofFun = Quotient.mk'

source

instance Filter.Germ.instCoeTCForAllGerm {α : Type u_1} {β : Type u_2} {l : Filter α} :

CoeTC (α → β) (Filter.Germ l β)

Equations

Filter.Germ.instCoeTCForAllGerm = { coe := Filter.Germ.ofFun }

source

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

Filter.Germ l β

Equations

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

source

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

CoeTC β (Filter.Germ l β)

Equations

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

source

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

Prop

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

Equations

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

source

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

Filter.Germ.IsConstant ↑f

source

@[simp]

theorem Filter.Germ.isConstant_coe_const {α : Type u_1} {β : Type u_2} {l : Filter α} {b : β} :

Filter.Germ.IsConstant ↑fun (x : α) => b

source

theorem Filter.Germ.isConstant_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {g : β → γ} (h : Filter.Germ.IsConstant ↑f) :

Filter.Germ.IsConstant ↑(g ∘ f)

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

source

@[simp]

theorem Filter.Germ.quot_mk_eq_coe {α : Type u_1} {β : Type u_2} (l : Filter α) (f : α → β) :

Quot.mk Setoid.r f = ↑f

source

@[simp]

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

Quotient.mk' f = ↑f

source

theorem Filter.Germ.inductionOn {α : Type u_1} {β : Type u_2} {l : Filter α} (f : Filter.Germ l β) {p : Filter.Germ l β → Prop} (h : ∀ (f : α → β), p ↑f) :

p f

source

theorem Filter.Germ.inductionOn₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : Filter.Germ l β) (g : Filter.Germ l γ) {p : Filter.Germ l β → Filter.Germ l γ → Prop} (h : ∀ (f : α → β) (g : α → γ), p ↑f ↑g) :

p f g

source

theorem Filter.Germ.inductionOn₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (f : Filter.Germ l β) (g : Filter.Germ l γ) (h : Filter.Germ l δ) {p : Filter.Germ l β → Filter.Germ l γ → Filter.Germ l δ → Prop} (H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p ↑f ↑g ↑h) :

p f g h

source

def Filter.Germ.map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (Filter.EventuallyEq l ⇒ Filter.EventuallyEq lc) F F) :

Filter.Germ l β → Filter.Germ lc δ

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

source

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

Filter.Germ.liftOn f F hF = Quotient.liftOn' f F hF

source

@[simp]

theorem Filter.Germ.map'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (Filter.EventuallyEq l ⇒ Filter.EventuallyEq lc) F F) (f : α → β) :

Filter.Germ.map' F hF ↑f = ↑(F f)

source

@[simp]

theorem Filter.Germ.coe_eq {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {g : α → β} :

↑f = ↑g ↔ f =ᶠ[l] g

source

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.

source

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

Filter.Germ l β → Filter.Germ l γ

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

Equations

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

source

@[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)

source

@[simp]

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

Filter.Germ.map id = id

source

theorem Filter.Germ.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op₁ : γ → δ) (op₂ : β → γ) (f : Filter.Germ l β) :

Filter.Germ.map op₁ (Filter.Germ.map op₂ f) = Filter.Germ.map (op₁ ∘ op₂) f

source

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

Filter.Germ l β → Filter.Germ l γ → Filter.Germ l δ

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)) ⋯

source

@[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)

source

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

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

source

@[simp]

theorem Filter.Germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β} :

Filter.Germ.Tendsto (↑f) lb ↔ Filter.Tendsto f l lb

source

theorem Filter.Tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β} :

Filter.Tendsto f l lb → Filter.Germ.Tendsto (↑f) lb

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

source

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

Filter.Germ lc β

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

Filter.Germ.compTendsto' f g hg = Filter.Germ.liftOn f (fun (f : α → β) => Filter.Germ.map f g) ⋯

source

@[simp]

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

Filter.Germ.compTendsto' (↑f) g hg = Filter.Germ.map f g

source

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

Filter.Germ lc β

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

Filter.Germ.compTendsto f g hg = Filter.Germ.compTendsto' f ↑g ⋯

source

@[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) :

Filter.Germ.compTendsto (↑f) g hg = ↑(f ∘ g)

source

@[simp]

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

Filter.Germ.compTendsto' f ↑g ⋯ = Filter.Germ.compTendsto f g hg

source

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 ∘ φ)

source

theorem Filter.Germ.isConstant_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {lc : Filter γ} {g : γ → α} (hf : Filter.Germ.IsConstant ↑f) (hg : Filter.Tendsto g lc l) :

Filter.Germ.IsConstant ↑(f ∘ g)

source

theorem Filter.Germ.isConstant_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : Filter.Germ l β} {lc : Filter γ} {g : γ → α} (hf : Filter.Germ.IsConstant f) (hg : Filter.Tendsto g lc l) :

Filter.Germ.IsConstant (Filter.Germ.compTendsto f g hg)

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.

source

@[simp]

theorem Filter.Germ.const_inj {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :

↑a = ↑b ↔ a = b

source

@[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)

source

@[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)

source

@[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) :

Filter.Germ.compTendsto (↑b) g hg = ↑b

source

@[simp]

theorem Filter.Germ.const_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (b : β) {lc : Filter γ} {g : Filter.Germ lc α} (hg : Filter.Germ.Tendsto g l) :

Filter.Germ.compTendsto' (↑b) g hg = ↑b

source

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

Prop

Lift a predicate on β to Germ l β.

Equations

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

source

@[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)

source

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

Filter.Germ.LiftPred p ↑x

source

@[simp]

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

Filter.Germ.LiftPred p ↑x ↔ p x

source

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

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)) ⋯

source

@[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)

source

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

source

@[simp]

theorem Filter.Germ.liftRel_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} [Filter.NeBot l] {r : β → γ → Prop} {x : β} {y : γ} :

Filter.Germ.LiftRel r ↑x ↑y ↔ r x y

source

instance Filter.Germ.inhabited {α : Type u_1} {β : Type u_2} {l : Filter α} [Inhabited β] :

Inhabited (Filter.Germ l β)

Equations

Filter.Germ.inhabited = { default := ↑default }

source

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

Add (Filter.Germ l M)

Equations

Filter.Germ.add = { add := Filter.Germ.map₂ fun (x x_1 : M) => x + x_1 }

source

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

Mul (Filter.Germ l M)

Equations

Filter.Germ.mul = { mul := Filter.Germ.map₂ fun (x x_1 : M) => x * x_1 }

source

@[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

source

@[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

source

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

Zero (Filter.Germ l M)

Equations

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

source

instance Filter.Germ.one {α : Type u_1} {l : Filter α} {M : Type u_5} [One M] :

One (Filter.Germ l M)

Equations

Filter.Germ.one = { one := ↑1 }

source

@[simp]

theorem Filter.Germ.coe_zero {α : Type u_1} {l : Filter α} {M : Type u_5} [Zero M] :

↑0 = 0

source

@[simp]

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

↑1 = 1

source

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

a + b + c = a + (b + c)

source

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

AddSemigroup (Filter.Germ l M)

Equations

Filter.Germ.addSemigroup = AddSemigroup.mk ⋯

source

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

Semigroup (Filter.Germ l M)

Equations

Filter.Germ.semigroup = Semigroup.mk ⋯

source

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

q₁ + q₂ = q₂ + q₁

source

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

AddCommSemigroup (Filter.Germ l M)

Equations

Filter.Germ.addCommSemigroup = AddCommSemigroup.mk ⋯

source

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

CommSemigroup (Filter.Germ l M)

Equations

Filter.Germ.commSemigroup = CommSemigroup.mk ⋯

source

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

IsLeftCancelAdd (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

IsLeftCancelMul (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

IsRightCancelAdd (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

IsRightCancelMul (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

IsCancelAdd (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

IsCancelMul (Filter.Germ l M)

Equations

⋯ = ⋯

source

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

AddLeftCancelSemigroup (Filter.Germ l M)

Equations

Filter.Germ.addLeftCancelSemigroup = let __src := Filter.Germ.addSemigroup; AddLeftCancelSemigroup.mk ⋯

source

theorem Filter.Germ.addLeftCancelSemigroup.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddLeftCancelSemigroup M] :

∀ (x x_1 x_2 : Filter.Germ l M), x + x_1 = x + x_2 → x_1 = x_2

source

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

LeftCancelSemigroup (Filter.Germ l M)

Equations

Filter.Germ.leftCancelSemigroup = let __src := Filter.Germ.semigroup; LeftCancelSemigroup.mk ⋯

source

theorem Filter.Germ.addRightCancelSemigroup.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddRightCancelSemigroup M] :

∀ (x x_1 x_2 : Filter.Germ l M), x + x_1 = x_2 + x_1 → x = x_2

source

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

AddRightCancelSemigroup (Filter.Germ l M)

Equations

Filter.Germ.addRightCancelSemigroup = let __src := Filter.Germ.addSemigroup; AddRightCancelSemigroup.mk ⋯

source

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

RightCancelSemigroup (Filter.Germ l M)

Equations

Filter.Germ.rightCancelSemigroup = let __src := Filter.Germ.semigroup; RightCancelSemigroup.mk ⋯

source

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

q + 0 = q

source

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

0 + q = q

source

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

AddZeroClass (Filter.Germ l M)

Equations

Filter.Germ.addZeroClass = AddZeroClass.mk ⋯ ⋯

source

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

MulOneClass (Filter.Germ l M)

Equations

Filter.Germ.mulOneClass = MulOneClass.mk ⋯ ⋯

source

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

VAdd M (Filter.Germ l G)

Equations

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

source

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

SMul M (Filter.Germ l G)

Equations

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

source

instance Filter.Germ.pow {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [Pow G M] :

Pow (Filter.Germ l G) M

Equations

Filter.Germ.pow = { pow := fun (f : Filter.Germ l G) (n : M) => Filter.Germ.map (fun (x : G) => x ^ n) f }

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

theorem Filter.Germ.addMonoid.proof_2 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :

↑0 = ↑0

source

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

AddMonoid.nsmul 0 x = 0

source

theorem Filter.Germ.addMonoid.proof_4 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :

∀ (x : α → M) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem Filter.Germ.addMonoid.proof_3 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :

∀ (x x_1 : α → M), ↑(x + x_1) = ↑(x + x_1)

source

theorem Filter.Germ.addMonoid.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} :

Function.Surjective (Quot.mk Setoid.r)

source

theorem Filter.Germ.addMonoid.proof_8 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] (n : ℕ) (x : Filter.Germ l M) :

AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

source

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

0 + a = a

source

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

a + 0 = a

source

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

AddMonoid (Filter.Germ l M)

Equations

Filter.Germ.addMonoid = let __src := Function.Surjective.addMonoid Filter.Germ.ofFun ⋯ ⋯ ⋯ ⋯; AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : Filter.Germ l M) => n • a) ⋯ ⋯

source

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

Monoid (Filter.Germ l M)

Equations

Filter.Germ.monoid = let __src := Function.Surjective.monoid Filter.Germ.ofFun ⋯ ⋯ ⋯ ⋯; Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : Filter.Germ l M) => a ^ n) ⋯ ⋯

source

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)

source

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

(α → M) →+ Filter.Germ l M

Coercion from functions to germs as an additive monoid homomorphism.

Equations

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

source

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

↑0 = ↑0

source

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

(α → M) →* Filter.Germ l M

Coercion from functions to germs as a monoid homomorphism.

Equations

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

source

@[simp]

theorem Filter.Germ.coe_coeAddHom {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoid M] :

⇑(Filter.Germ.coeAddHom l) = Filter.Germ.ofFun

source

@[simp]

theorem Filter.Germ.coe_coeMulHom {α : Type u_1} {l : Filter α} {M : Type u_5} [Monoid M] :

⇑(Filter.Germ.coeMulHom l) = Filter.Germ.ofFun

source

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

AddCommMonoid (Filter.Germ l M)

Equations

Filter.Germ.addCommMonoid = AddCommMonoid.mk ⋯

source

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

a + b = b + a

source

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

CommMonoid (Filter.Germ l M)

Equations

Filter.Germ.commMonoid = CommMonoid.mk ⋯

source

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

NatCast (Filter.Germ l M)

Equations

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

source

@[simp]

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

(↑fun (x : α) => ↑n) = ↑n

source

@[simp]

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

↑↑n = ↑n

source

@[simp]

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

↑(OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

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

↑(OfNat.ofNat n) = OfNat.ofNat n

source

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

IntCast (Filter.Germ l M)

Equations

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

source

@[simp]

theorem Filter.Germ.coe_int {α : Type u_1} {l : Filter α} {M : Type u_5} [IntCast M] (n : ℤ) :

(↑fun (x : α) => ↑n) = ↑n

source

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

AddMonoidWithOne (Filter.Germ l M)

Equations

Filter.Germ.addMonoidWithOne = let __src := Filter.Germ.natCast; let __src_1 := Filter.Germ.addMonoid; let __src_2 := Filter.Germ.one; AddMonoidWithOne.mk ⋯ ⋯

source

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

AddCommMonoidWithOne (Filter.Germ l M)

Equations

Filter.Germ.addCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

source

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

Neg (Filter.Germ l G)

Equations

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

source

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

Inv (Filter.Germ l G)

Equations

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

source

@[simp]

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

↑(-f) = -↑f

source

@[simp]

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

↑f⁻¹ = (↑f)⁻¹

source

@[simp]

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

↑(-a) = -↑a

source

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

source

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

Sub (Filter.Germ l M)

Equations

Filter.Germ.sub = { sub := Filter.Germ.map₂ fun (x x_1 : M) => x - x_1 }

source

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

Div (Filter.Germ l M)

Equations

Filter.Germ.div = { div := Filter.Germ.map₂ fun (x x_1 : M) => x / x_1 }

source

@[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

source

@[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

source

@[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

source

@[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

source

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

- -q = q

source

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

InvolutiveNeg (Filter.Germ l G)

Equations

Filter.Germ.involutiveNeg = InvolutiveNeg.mk ⋯

source

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

InvolutiveInv (Filter.Germ l G)

Equations

Filter.Germ.involutiveInv = InvolutiveInv.mk ⋯

source

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

HasDistribNeg (Filter.Germ l G)

Equations

Filter.Germ.hasDistribNeg = HasDistribNeg.mk ⋯ ⋯

source

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

NegZeroClass (Filter.Germ l G)

Equations

Filter.Germ.negZeroClass = NegZeroClass.mk ⋯

source

theorem Filter.Germ.negZeroClass.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [NegZeroClass G] :

↑((fun (x : α → G) => Neg.neg ∘ x) fun (x : α) => 0) = ↑fun (x : α) => 0

source

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

InvOneClass (Filter.Germ l G)

Equations

Filter.Germ.invOneClass = InvOneClass.mk ⋯

source

theorem Filter.Germ.subNegMonoid.proof_2 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] (q : Quotient (Filter.germSetoid l G)) :

(fun (z : ℤ) (f : Filter.Germ l G) => z • f) 0 q = 0

source

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

SubNegMonoid (Filter.Germ l G)

Equations

One or more equations did not get rendered due to their size.

source

theorem Filter.Germ.subNegMonoid.proof_3 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] :

∀ (x : ℕ) (q : Quotient (Filter.germSetoid l G)), (fun (z : ℤ) (f : Filter.Germ l G) => z • f) (Int.ofNat (Nat.succ x)) q = (fun (z : ℤ) (f : Filter.Germ l G) => z • f) (Int.ofNat x) q + q

source

theorem Filter.Germ.subNegMonoid.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] (q₁ : Quotient (Filter.germSetoid l G)) (q₂ : Quotient (Filter.germSetoid l G)) :

q₁ - q₂ = q₁ + -q₂

source

theorem Filter.Germ.subNegMonoid.proof_4 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] :

∀ (x : ℕ) (q : Quotient (Filter.germSetoid l G)), (fun (z : ℤ) (f : Filter.Germ l G) => z • f) (Int.negSucc x) q = -(fun (z : ℤ) (f : Filter.Germ l G) => z • f) (↑(Nat.succ x)) q

source

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

DivInvMonoid (Filter.Germ l G)

Equations

One or more equations did not get rendered due to their size.

source

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

-(x + y) = -y + -x

source

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

- -a = a

source

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

SubtractionMonoid (Filter.Germ l G)

Equations

Filter.Germ.divisionAddMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

source

theorem Filter.Germ.divisionAddMonoid.proof_3 {α : Type u_2} {l : Filter α} {G : Type u_1} [SubtractionMonoid G] (x : Filter.Germ l G) (y : Filter.Germ l G) :

x + y = 0 → -x = y

source

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

DivisionMonoid (Filter.Germ l G)

Equations

Filter.Germ.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

source

theorem Filter.Germ.addGroup.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [AddGroup G] (q : Quotient (Filter.germSetoid l G)) :

-q + q = 0

source

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

AddGroup (Filter.Germ l G)

Equations

Filter.Germ.addGroup = AddGroup.mk ⋯

source

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

Group (Filter.Germ l G)

Equations

Filter.Germ.group = Group.mk ⋯

source

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

a + b = b + a

source

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

AddCommGroup (Filter.Germ l G)

Equations

Filter.Germ.addCommGroup = AddCommGroup.mk ⋯

source

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

CommGroup (Filter.Germ l G)

Equations

Filter.Germ.commGroup = CommGroup.mk ⋯

source

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

AddGroupWithOne (Filter.Germ l G)

Equations

One or more equations did not get rendered due to their size.

source

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

Nontrivial (Filter.Germ l R)

Equations

⋯ = ⋯

source

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

MulZeroClass (Filter.Germ l R)

Equations

Filter.Germ.mulZeroClass = MulZeroClass.mk ⋯ ⋯

source

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

MulZeroOneClass (Filter.Germ l R)

Equations

Filter.Germ.mulZeroOneClass = let __src := Filter.Germ.mulZeroClass; let __src_1 := Filter.Germ.mulOneClass; MulZeroOneClass.mk ⋯ ⋯

source

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

MonoidWithZero (Filter.Germ l R)

Equations

Filter.Germ.monoidWithZero = let __src := Filter.Germ.monoid; let __src_1 := Filter.Germ.mulZeroClass; MonoidWithZero.mk ⋯ ⋯

source

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

Distrib (Filter.Germ l R)

Equations

Filter.Germ.distrib = Distrib.mk ⋯ ⋯

source

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

NonUnitalNonAssocSemiring (Filter.Germ l R)

Equations

One or more equations did not get rendered due to their size.

source

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

NonUnitalSemiring (Filter.Germ l R)

Equations

Filter.Germ.nonUnitalSemiring = NonUnitalSemiring.mk ⋯

source

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

NonAssocSemiring (Filter.Germ l R)

Equations

One or more equations did not get rendered due to their size.

source

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

NonUnitalNonAssocRing (Filter.Germ l R)

Equations

Filter.Germ.nonUnitalNonAssocRing = let __src := Filter.Germ.addCommGroup; let __src_1 := Filter.Germ.nonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

source

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

NonUnitalRing (Filter.Germ l R)

Equations

Filter.Germ.nonUnitalRing = NonUnitalRing.mk ⋯

source

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

NonAssocRing (Filter.Germ l R)

Equations

Filter.Germ.nonAssocRing = let __src := Filter.Germ.nonUnitalNonAssocRing; let __src_1 := Filter.Germ.nonAssocSemiring; let __src_2 := Filter.Germ.addGroupWithOne; NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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

Semiring (Filter.Germ l R)

Equations

Filter.Germ.semiring = let __src := Filter.Germ.nonUnitalSemiring; let __src_1 := Filter.Germ.nonAssocSemiring; let __src_2 := Filter.Germ.monoidWithZero; Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

source

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

Ring (Filter.Germ l R)

Equations

Filter.Germ.ring = let __src := Filter.Germ.semiring; let __src_1 := Filter.Germ.addCommGroup; let __src_2 := Filter.Germ.nonAssocRing; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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

NonUnitalCommSemiring (Filter.Germ l R)

Equations

Filter.Germ.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

source

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

CommSemiring (Filter.Germ l R)

Equations

Filter.Germ.commSemiring = CommSemiring.mk ⋯

source

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

NonUnitalCommRing (Filter.Germ l R)

Equations

Filter.Germ.nonUnitalCommRing = let __src := Filter.Germ.nonUnitalRing; let __src_1 := Filter.Germ.commSemigroup; NonUnitalCommRing.mk ⋯

source

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

CommRing (Filter.Germ l R)

Equations

Filter.Germ.commRing = CommRing.mk ⋯

source

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

(α → R) →+* Filter.Germ l R

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

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Filter.Germ.coe_coeRingHom {α : Type u_1} {l : Filter α} {R : Type u_5} [Semiring R] :

⇑(Filter.Germ.coeRingHom l) = Filter.Germ.ofFun

source

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

VAdd (Filter.Germ l M) (Filter.Germ l β)

Equations

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

source

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

SMul (Filter.Germ l M) (Filter.Germ l β)

Equations

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

source

@[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

source

@[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

source

theorem Filter.Germ.addAction.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (f : Filter.Germ l β) :

0 +ᵥ f = f

source

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

AddAction M (Filter.Germ l β)

Equations

Filter.Germ.addAction = AddAction.mk ⋯ ⋯

source

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

c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)

source

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

MulAction M (Filter.Germ l β)

Equations

Filter.Germ.mulAction = MulAction.mk ⋯ ⋯

source

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

AddAction (Filter.Germ l M) (Filter.Germ l β)

Equations

Filter.Germ.addAction' = AddAction.mk ⋯ ⋯

source

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

0 +ᵥ f = f

source

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

c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)

source

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

MulAction (Filter.Germ l M) (Filter.Germ l β)

Equations

Filter.Germ.mulAction' = MulAction.mk ⋯ ⋯

source

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

DistribMulAction M (Filter.Germ l N)

Equations

Filter.Germ.distribMulAction = DistribMulAction.mk ⋯ ⋯

source

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

DistribMulAction (Filter.Germ l M) (Filter.Germ l N)

Equations

Filter.Germ.distribMulAction' = DistribMulAction.mk ⋯ ⋯

source

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

Module R (Filter.Germ l M)

Equations

Filter.Germ.module = Module.mk ⋯ ⋯

source

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

Module (Filter.Germ l R) (Filter.Germ l M)

Equations

Filter.Germ.module' = Module.mk ⋯ ⋯

source

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

LE (Filter.Germ l β)

Equations

Filter.Germ.le = { le := Filter.Germ.LiftRel fun (x x_1 : β) => x ≤ x_1 }

source

theorem Filter.Germ.le_def {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] :

(fun (x x_1 : Filter.Germ l β) => x ≤ x_1) = Filter.Germ.LiftRel fun (x x_1 : β) => x ≤ x_1

source

@[simp]

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

↑f ≤ ↑g ↔ f ≤ᶠ[l] g

source

theorem Filter.Germ.coe_nonneg {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [Zero β] {f : α → β} :

0 ≤ ↑f ↔ ∀ᶠ (x : α) in l, 0 ≤ f x

source

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

x ≤ y → ↑x ≤ ↑y

source

@[simp]

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

↑x ≤ ↑y ↔ x ≤ y

source

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

Preorder (Filter.Germ l β)

Equations

Filter.Germ.preorder = Preorder.mk ⋯ ⋯ ⋯

source

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

PartialOrder (Filter.Germ l β)

Equations

Filter.Germ.partialOrder = let __src := Filter.Germ.preorder; PartialOrder.mk ⋯

source

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

Bot (Filter.Germ l β)

Equations

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

source

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

Top (Filter.Germ l β)

Equations

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

source

@[simp]

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

↑⊥ = ⊥

source

@[simp]

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

↑⊤ = ⊤

source

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

OrderBot (Filter.Germ l β)

Equations

Filter.Germ.orderBot = OrderBot.mk ⋯

source

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

OrderTop (Filter.Germ l β)

Equations

Filter.Germ.orderTop = OrderTop.mk ⋯

source

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

BoundedOrder (Filter.Germ l β)

Equations

Filter.Germ.instBoundedOrderGermLe = let __src := Filter.Germ.orderBot; let __src_1 := Filter.Germ.orderTop; BoundedOrder.mk

source

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

Sup (Filter.Germ l β)

Equations

Filter.Germ.sup = { sup := Filter.Germ.map₂ fun (x x_1 : β) => x ⊔ x_1 }

source

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

Inf (Filter.Germ l β)

Equations

Filter.Germ.inf = { inf := Filter.Germ.map₂ fun (x x_1 : β) => x ⊓ x_1 }

source

@[simp]

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

↑(a ⊔ b) = ↑a ⊔ ↑b

source

@[simp]

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

↑(a ⊓ b) = ↑a ⊓ ↑b

source

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

SemilatticeSup (Filter.Germ l β)

Equations

Filter.Germ.semilatticeSup = let __src := Filter.Germ.partialOrder; SemilatticeSup.mk ⋯ ⋯ ⋯

source

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

SemilatticeInf (Filter.Germ l β)

Equations

Filter.Germ.semilatticeInf = let __src := Filter.Germ.partialOrder; SemilatticeInf.mk ⋯ ⋯ ⋯

source

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

Lattice (Filter.Germ l β)

Equations

Filter.Germ.lattice = let __src := Filter.Germ.semilatticeSup; let __src_1 := Filter.Germ.semilatticeInf; Lattice.mk ⋯ ⋯ ⋯

source

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

DistribLattice (Filter.Germ l β)

Equations

Filter.Germ.distribLattice = let __src := Filter.Germ.semilatticeSup; let __src_1 := Filter.Germ.semilatticeInf; DistribLattice.mk ⋯

source

theorem Filter.Germ.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommMonoid β] (f : Filter.Germ l β) (g : Filter.Germ l β) :

f ≤ g → ∀ (c : Filter.Germ l β), c + f ≤ c + g

source

instance Filter.Germ.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommMonoid β] :

OrderedAddCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.orderedAddCommMonoid = let __src := Filter.Germ.partialOrder; let __src_1 := Filter.Germ.addCommMonoid; OrderedAddCommMonoid.mk ⋯

source

instance Filter.Germ.orderedCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommMonoid β] :

OrderedCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.orderedCommMonoid = let __src := Filter.Germ.partialOrder; let __src_1 := Filter.Germ.commMonoid; OrderedCommMonoid.mk ⋯

source

theorem Filter.Germ.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedCancelAddCommMonoid β] (f : Filter.Germ l β) (g : Filter.Germ l β) (h : Filter.Germ l β) :

f + g ≤ f + h → g ≤ h

source

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

OrderedCancelAddCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.orderedAddCancelCommMonoid = let __src := Filter.Germ.orderedAddCommMonoid; OrderedCancelAddCommMonoid.mk ⋯

source

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

OrderedCancelCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.orderedCancelCommMonoid = let __src := Filter.Germ.orderedCommMonoid; OrderedCancelCommMonoid.mk ⋯

source

theorem Filter.Germ.orderedAddCommGroup.proof_2 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) :

SubNegMonoid.zsmul 0 a = 0

source

theorem Filter.Germ.orderedAddCommGroup.proof_6 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :

a + b = b + a

source

theorem Filter.Germ.orderedAddCommGroup.proof_4 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (n : ℕ) (a : Filter.Germ l β) :

SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

source

theorem Filter.Germ.orderedAddCommGroup.proof_7 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :

a ≤ b → ∀ (c : Filter.Germ l β), c + a ≤ c + b

source

theorem Filter.Germ.orderedAddCommGroup.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :

a - b = a + -b

source

theorem Filter.Germ.orderedAddCommGroup.proof_5 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) :

-a + a = 0

source

instance Filter.Germ.orderedAddCommGroup {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] :

OrderedAddCommGroup (Filter.Germ l β)

Equations

Filter.Germ.orderedAddCommGroup = let __src := Filter.Germ.orderedAddCancelCommMonoid; let __src_1 := Filter.Germ.addCommGroup; OrderedAddCommGroup.mk ⋯

source

theorem Filter.Germ.orderedAddCommGroup.proof_3 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (n : ℕ) (a : Filter.Germ l β) :

SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = SubNegMonoid.zsmul (Int.ofNat n) a + a

source

instance Filter.Germ.orderedCommGroup {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommGroup β] :

OrderedCommGroup (Filter.Germ l β)

Equations

Filter.Germ.orderedCommGroup = let __src := Filter.Germ.orderedCancelCommMonoid; let __src_1 := Filter.Germ.commGroup; OrderedCommGroup.mk ⋯

source

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

ExistsAddOfLE (Filter.Germ l β)

Equations

⋯ = ⋯

source

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

ExistsMulOfLE (Filter.Germ l β)

Equations

⋯ = ⋯

source

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

CanonicallyOrderedAddCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.CanonicallyOrderedAddCommMonoid = let __src := Filter.Germ.orderedAddCommMonoid; let __src_1 := Filter.Germ.orderBot; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

source

theorem Filter.Germ.CanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} {l : Filter α} [CanonicallyOrderedAddCommMonoid β] :

∀ {a b : Filter.Germ l β}, a ≤ b → ∃ (c : Filter.Germ l β), b = a + c

source

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

ExistsAddOfLE (Filter.Germ l β)

source

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

x ≤ x + y

source

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

CanonicallyOrderedCommMonoid (Filter.Germ l β)

Equations

Filter.Germ.CanonicallyOrderedCommMonoid = let __src := Filter.Germ.orderedCommMonoid; let __src_1 := Filter.Germ.orderBot; let __src_2 := ⋯; CanonicallyOrderedCommMonoid.mk ⋯ ⋯

source

instance Filter.Germ.orderedSemiring {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedSemiring β] :

OrderedSemiring (Filter.Germ l β)

Equations

Filter.Germ.orderedSemiring = let __src := Filter.Germ.semiring; let __src_1 := Filter.Germ.orderedAddCommMonoid; OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

source

instance Filter.Germ.orderedCommSemiring {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommSemiring β] :

OrderedCommSemiring (Filter.Germ l β)

Equations

Filter.Germ.orderedCommSemiring = let __src := Filter.Germ.orderedSemiring; let __src_1 := Filter.Germ.commSemiring; OrderedCommSemiring.mk ⋯

source

instance Filter.Germ.orderedRing {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedRing β] :

OrderedRing (Filter.Germ l β)

Equations

Filter.Germ.orderedRing = let __src := Filter.Germ.ring; let __src_1 := Filter.Germ.orderedAddCommGroup; OrderedRing.mk ⋯ ⋯ ⋯

source

instance Filter.Germ.orderedCommRing {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommRing β] :

OrderedCommRing (Filter.Germ l β)

Equations

Filter.Germ.orderedCommRing = let __src := Filter.Germ.orderedRing; let __src_1 := Filter.Germ.orderedCommSemiring; OrderedCommRing.mk ⋯

Documentation

Mathlib.Order.Filter.Germ

Germ of a function at a filter #

Main definitions #

Tags #