mathlib documentation

order.filter.germ

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 eventually_eq l: f ≈ g means ∀ᶠ x in l, f x = g x.

Main definitions

We define

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

Tags

filter, germ

theorem filter.const_eventually_eq' {α : Type u_1} {β : Type u_2} {l : filter α} [l.ne_bot] {a b : β} :
(∀ᶠ (x : α) in l, a = b) a = b

theorem filter.const_eventually_eq {α : Type u_1} {β : Type u_2} {l : filter α} [l.ne_bot] {a b : β} :
((λ (_x : α), a) =ᶠ[l] λ (_x : α), b) a = b

theorem filter.eventually_eq.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} {f f' : α → β} (H : f =ᶠ[l] f') {g : γ → α} {lc : filter γ} :
filter.tendsto g lc lf g =ᶠ[lc] f' g

def filter.germ_setoid {α : Type u_1} (l : filter α) (β : Type u_2) :
setoid (α → β)

Setoid used to define the space of germs.

Equations
def filter.germ {α : Type u_1} :
filter αType u_2Type (max u_1 u_2)

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

Equations
@[instance]
def filter.germ.has_coe_t {α : Type u_1} {β : Type u_2} {l : filter α} :
has_coe_t (α → β) (l.germ β)

Equations
@[instance]
def filter.germ.has_lift_t {α : Type u_1} {β : Type u_2} {l : filter α} :
has_lift_t β (l.germ β)

Equations
@[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 : α → β) :

theorem filter.germ.induction_on {α : Type u_1} {β : Type u_2} {l : filter α} (f : l.germ β) {p : l.germ β → Prop} :
(∀ (f : α → β), p f)p f

theorem filter.germ.induction_on₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : l.germ β) (g : l.germ γ) {p : l.germ βl.germ γ → Prop} :
(∀ (f : α → β) (g : α → γ), p f g)p f g

theorem filter.germ.induction_on₃ {α : 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} :
(∀ (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 : (α → β)γ → δ) :
(l.eventually_eq lc.eventually_eq) F Fl.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
def filter.germ.lift_on {α : Type u_1} {β : Type u_2} {l : filter α} {γ : Sort u_3} (f : l.germ β) (F : (α → β) → γ) :
(l.eventually_eq eq) 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
@[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.eventually_eq lc.eventually_eq) F F) (f : α → β) :

@[simp]
theorem filter.germ.coe_eq {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α → β} :
f = g f =ᶠ[l] g

def filter.germ.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} :
(β → γ)l.germ βl.germ γ

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

Equations
@[simp]
theorem filter.germ.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (op : β → γ) (f : α → β) :

@[simp]
theorem filter.germ.map_id {α : Type u_1} {β : Type u_2} {l : filter α} :

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 α} :
(β → γ → δ)l.germ βl.germ γl.germ δ

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

Equations
@[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 = (λ (x : α), op (f x) (g x))

def filter.germ.tendsto {α : Type u_1} {β : Type u_2} {l : filter α} :
l.germ β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
@[simp]
theorem filter.germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {lb : filter β} :

def filter.germ.comp_tendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : l.germ β) {lc : filter γ} (g : lc.germ α) :
g.tendsto llc.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
@[simp]
theorem filter.germ.coe_comp_tendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : α → β) {lc : filter γ} {g : lc.germ α} (hg : g.tendsto l) :

def filter.germ.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : l.germ β) {lc : filter γ} (g : γ → α) :
filter.tendsto g lc llc.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
@[simp]
theorem filter.germ.coe_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : α → β) {lc : filter γ} {g : γ → α} (hg : filter.tendsto g lc l) :
f.comp_tendsto g hg = (f g)

@[simp]
theorem filter.germ.comp_tendsto'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : l.germ β) {lc : filter γ} {g : γ → α} (hg : filter.tendsto g lc l) :

@[simp]
theorem filter.germ.const_inj {α : Type u_1} {β : Type u_2} {l : filter α} [l.ne_bot] {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 : β → γ) :

@[simp]
theorem filter.germ.map₂_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : filter α) (b : β) (c : γ) (f : β → γ → δ) :

@[simp]
theorem filter.germ.const_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (b : β) {lc : filter γ} {g : γ → α} (hg : filter.tendsto g lc l) :

@[simp]
theorem filter.germ.const_comp_tendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (b : β) {lc : filter γ} {g : lc.germ α} (hg : g.tendsto l) :

def filter.germ.lift_pred {α : Type u_1} {β : Type u_2} {l : filter α} :
(β → Prop)l.germ β → Prop

Lift a predicate on β to germ l β.

Equations
@[simp]
theorem filter.germ.lift_pred_coe {α : Type u_1} {β : Type u_2} {l : filter α} {p : β → Prop} {f : α → β} :
filter.germ.lift_pred p f ∀ᶠ (x : α) in l, p (f x)

theorem filter.germ.lift_pred_const {α : Type u_1} {β : Type u_2} {l : filter α} {p : β → Prop} {x : β} :

@[simp]
theorem filter.germ.lift_pred_const_iff {α : Type u_1} {β : Type u_2} {l : filter α} [l.ne_bot] {p : β → Prop} {x : β} :

def filter.germ.lift_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} :
(β → γ → Prop)l.germ βl.germ γ → Prop

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

Equations
@[simp]
theorem filter.germ.lift_rel_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} {r : β → γ → Prop} {f : α → β} {g : α → γ} :
filter.germ.lift_rel r f g ∀ᶠ (x : α) in l, r (f x) (g x)

theorem filter.germ.lift_rel_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} {r : β → γ → Prop} {x : β} {y : γ} :

@[simp]
theorem filter.germ.lift_rel_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} [l.ne_bot] {r : β → γ → Prop} {x : β} {y : γ} :

@[instance]
def filter.germ.inhabited {α : Type u_1} {β : Type u_2} {l : filter α} [inhabited β] :

Equations
@[instance]
def filter.germ.has_mul {α : Type u_1} {l : filter α} {M : Type u_5} [has_mul M] :

Equations
@[instance]
def filter.germ.has_add {α : Type u_1} {l : filter α} {M : Type u_5} [has_add M] :

@[simp]
theorem filter.germ.coe_add {α : Type u_1} {l : filter α} {M : Type u_5} [has_add M] (f g : α → M) :
(f + g) = f + g

@[simp]
theorem filter.germ.coe_mul {α : Type u_1} {l : filter α} {M : Type u_5} [has_mul M] (f g : α → M) :
f * g = (f) * g

@[instance]
def filter.germ.has_zero {α : Type u_1} {l : filter α} {M : Type u_5} [has_zero M] :

@[instance]
def filter.germ.has_one {α : Type u_1} {l : filter α} {M : Type u_5} [has_one M] :

Equations
@[simp]
theorem filter.germ.coe_zero {α : Type u_1} {l : filter α} {M : Type u_5} [has_zero M] :
0 = 0

@[simp]
theorem filter.germ.coe_one {α : Type u_1} {l : filter α} {M : Type u_5} [has_one M] :
1 = 1

@[instance]
def filter.germ.semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [semigroup M] :

Equations
@[instance]
def filter.germ.add_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [add_semigroup M] :

@[instance]
def filter.germ.comm_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [comm_semigroup M] :

Equations
@[instance]
def filter.germ.add_comm_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [add_comm_semigroup M] :

@[instance]

@[instance]

@[instance]
def filter.germ.add_monoid {α : Type u_1} {l : filter α} {M : Type u_5} [add_monoid M] :

@[instance]
def filter.germ.monoid {α : Type u_1} {l : filter α} {M : Type u_5} [monoid M] :
monoid (l.germ M)

Equations
def filter.germ.coe_add_hom {α : Type u_1} {M : Type u_5} [add_monoid M] (l : filter α) :
(α → M) →+ l.germ M

coercion from functions to germs as an additive monoid homomorphism.

def filter.germ.coe_mul_hom {α : 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
@[simp]
theorem filter.germ.coe_coe_add_hom {α : Type u_1} {l : filter α} {M : Type u_5} [add_monoid M] :

@[simp]
theorem filter.germ.coe_coe_mul_hom {α : Type u_1} {l : filter α} {M : Type u_5} [monoid M] :

@[instance]
def filter.germ.comm_monoid {α : Type u_1} {l : filter α} {M : Type u_5} [comm_monoid M] :

Equations
@[instance]
def filter.germ.add_comm_monoid {α : Type u_1} {l : filter α} {M : Type u_5} [add_comm_monoid M] :

@[instance]
def filter.germ.has_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] :

Equations
@[instance]
def filter.germ.has_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] :

@[simp]
theorem filter.germ.coe_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] (f : α → G) :

@[simp]
theorem filter.germ.coe_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] (f : α → G) :

@[instance]
def filter.germ.group {α : Type u_1} {l : filter α} {G : Type u_6} [group G] :
group (l.germ G)

Equations
@[instance]
def filter.germ.add_group {α : Type u_1} {l : filter α} {G : Type u_6} [add_group G] :

@[simp]
theorem filter.germ.coe_sub {α : Type u_1} {l : filter α} {G : Type u_6} [add_group G] (f g : α → G) :
(f - g) = f - g

@[instance]
def filter.germ.add_comm_group {α : Type u_1} {l : filter α} {G : Type u_6} [add_comm_group G] :

@[instance]
def filter.germ.comm_group {α : Type u_1} {l : filter α} {G : Type u_6} [comm_group G] :

Equations
@[instance]
def filter.germ.nontrivial {α : Type u_1} {l : filter α} {R : Type u_5} [nontrivial R] [l.ne_bot] :

@[instance]
def filter.germ.mul_zero_class {α : Type u_1} {l : filter α} {R : Type u_5} [mul_zero_class R] :

Equations
@[instance]
def filter.germ.distrib {α : Type u_1} {l : filter α} {R : Type u_5} [distrib R] :

Equations
def filter.germ.coe_ring_hom {α : Type u_1} {R : Type u_5} [semiring R] (l : filter α) :
(α → R) →+* l.germ R

Coercion (α → R) → germ l R as a ring_hom.

Equations
@[simp]
theorem filter.germ.coe_coe_ring_hom {α : Type u_1} {l : filter α} {R : Type u_5} [semiring R] :

@[instance]
def filter.germ.has_scalar {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_scalar M β] :
has_scalar M (l.germ β)

Equations
@[instance]
def filter.germ.has_scalar' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_scalar M β] :
has_scalar (l.germ M) (l.germ β)

Equations
@[simp]
theorem filter.germ.coe_smul {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_scalar 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} [has_scalar M β] (c : α → M) (f : α → β) :
(c f) = c f

@[instance]
def filter.germ.mul_action {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [monoid M] [mul_action M β] :
mul_action M (l.germ β)

Equations
@[instance]
def filter.germ.mul_action' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [monoid M] [mul_action M β] :
mul_action (l.germ M) (l.germ β)

Equations
@[instance]
def filter.germ.semimodule {α : Type u_1} {l : filter α} {M : Type u_5} {R : Type u_7} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def filter.germ.semimodule' {α : Type u_1} {l : filter α} {M : Type u_5} {R : Type u_7} [semiring R] [add_comm_monoid M] [semimodule R M] :
semimodule (l.germ R) (l.germ M)

Equations
@[instance]
def filter.germ.has_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :
has_le (l.germ β)

Equations
@[simp]
theorem filter.germ.coe_le {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α → β} [has_le β] :

theorem filter.germ.const_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] {x y : β} :
x yx y

@[simp]
theorem filter.germ.const_le_iff {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [l.ne_bot] {x y : β} :
x y x y

@[instance]
def filter.germ.preorder {α : Type u_1} {β : Type u_2} {l : filter α} [preorder β] :
preorder (l.germ β)

Equations
@[instance]
def filter.germ.partial_order {α : Type u_1} {β : Type u_2} {l : filter α} [partial_order β] :

Equations
@[instance]
def filter.germ.has_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :
has_bot (l.germ β)

Equations
@[simp]
theorem filter.germ.const_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :

@[instance]
def filter.germ.order_bot {α : Type u_1} {β : Type u_2} {l : filter α} [order_bot β] :

Equations
@[instance]
def filter.germ.has_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :
has_top (l.germ β)

Equations
@[simp]
theorem filter.germ.const_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :

@[instance]
def filter.germ.order_top {α : Type u_1} {β : Type u_2} {l : filter α} [order_top β] :

Equations
@[instance]
def filter.germ.has_sup {α : Type u_1} {β : Type u_2} {l : filter α} [has_sup β] :
has_sup (l.germ β)

Equations
@[simp]
theorem filter.germ.const_sup {α : Type u_1} {β : Type u_2} {l : filter α} [has_sup β] (a b : β) :
(a b) = a b

@[instance]
def filter.germ.has_inf {α : Type u_1} {β : Type u_2} {l : filter α} [has_inf β] :
has_inf (l.germ β)

Equations
@[simp]
theorem filter.germ.const_inf {α : Type u_1} {β : Type u_2} {l : filter α} [has_inf β] (a b : β) :
(a b) = a b

@[instance]

@[instance]
def filter.germ.ordered_add_comm_group {α : Type u_1} {β : Type u_2} {l : filter α} [ordered_add_comm_group β] :