Germ of a function at a filter #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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 has_coe_t, so it does not require an explicit up arrow ↑;
coercion from β to germ l β: (↑c : germ l β) is the germ of the constant function λ x:α, c at a filter l; this coercion is declared as has_lift_t, so it requires an explicit up arrow ↑, see [TPiL][TPiL_coe] for details.
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 λ 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.comp_tendsto g hg and f.comp_tendsto' 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.lift_pred, germ.lift_rel: lift a predicate or a relation to the space of germs: (f : germ l β).lift_pred p means ∀ᶠ x in l, p (f x), and similarly for a relation. [TPiL_coe]: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes

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 comm_group;
mul_zero_class, distrib, semiring, comm_semiring, ring, comm_ring;
mul_action, distrib_mul_action, module;
preorder, partial_order, and lattice structures, as well as bounded_order;
ordered_cancel_comm_monoid and ordered_cancel_add_comm_monoid.

Tags #

filter, germ

source

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

source

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

source

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 γ} (hg : filter.tendsto g lc l) :

f ∘ g =ᶠ[lc] f' ∘ g

source

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

setoid (α → β)

Setoid used to define the space of germs.

Equations

l.germ_setoid β = {r := l.eventually_eq, iseqv := _}

source

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

Type (max u_1 u_2)

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

Equations

l.germ β = quotient (l.germ_setoid β)

Instances for filter.germ

source

def filter.product_setoid {α : Type u_1} (l : filter α) (ε : α → Type u_2) :

setoid (Π (a : α), ε a)

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

Equations

l.product_setoid ε = {r := λ (f g : Π (a : α), ε a), ∀ᶠ (a : α) in l, f a = g a, iseqv := _}

Instances for filter.product_setoid

first_order.language.ultraproduct.setoid_prestructure

source

@[protected]

def filter.product {α : Type u_1} (l : filter α) (ε : α → Type u_2) :

Type (max u_1 u_2)

The filter product Π (a : α), ε a at a filter l. This is a dependent version of filter.germ.

Equations

l.product ε = quotient (l.product_setoid ε)

Instances for filter.product

source

@[protected, instance]

def filter.product.has_coe_t {α : Type u_1} {l : filter α} {ε : α → Type u_5} :

has_coe_t (Π (a : α), ε a) (l.product ε)

Equations

filter.product.has_coe_t = {coe := quotient.mk' (l.product_setoid ε)}

source

@[protected, instance]

def filter.product.inhabited {α : Type u_1} {l : filter α} {ε : α → Type u_5} [Π (a : α), inhabited (ε a)] :

inhabited (l.product ε)

Equations

filter.product.inhabited = {default := ↑(λ (a : α), inhabited.default)}

source

@[protected, instance]

def filter.germ.has_coe_t {α : Type u_1} {β : Type u_2} {l : filter α} :

has_coe_t (α → β) (l.germ β)

Equations

filter.germ.has_coe_t = {coe := quotient.mk' (l.germ_setoid β)}

source

@[protected, instance]

def filter.germ.has_lift_t {α : Type u_1} {β : Type u_2} {l : filter α} :

has_lift_t β (l.germ β)

Equations

filter.germ.has_lift_t = {lift := λ (c : β), ↑(λ (x : α), c)}

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.induction_on {α : Type u_1} {β : Type u_2} {l : filter α} (f : l.germ β) {p : l.germ β → Prop} (h : ∀ (f : α → β), p ↑f) :

p f

source

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} (h : ∀ (f : α → β) (g : α → γ), p ↑f ↑g) :

p f g

source

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} (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 : (l.eventually_eq ⇒ lc.eventually_eq) 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

source

def filter.germ.lift_on {α : Type u_1} {β : Type u_2} {l : filter α} {γ : Sort u_3} (f : l.germ β) (F : (α → β) → γ) (hF : (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

f.lift_on F hF = quotient.lift_on' 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 : (l.eventually_eq ⇒ lc.eventually_eq) F F) (f : α → β) :

filter.germ.map' F hF ↑f = ↑(F f)

source

@[simp, norm_cast]

theorem filter.germ.coe_eq {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α → β} :

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

source

theorem filter.eventually_eq.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 : β → γ) :

l.germ β → l.germ γ

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

Equations

filter.germ.map op = filter.germ.map' (function.comp op) _

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 : l.germ β) :

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 : β → γ → δ) :

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₂' (λ (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 = ↑(λ (x : α), op (f x) (g x))

source

@[protected]

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.lift_on (λ (f : α → β), filter.tendsto f l lb) _

source

@[simp, norm_cast]

theorem filter.germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {lb : filter β} :

↑f.tendsto 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 → ↑f.tendsto lb

Alias of the reverse direction of filter.germ.coe_tendsto.

source

def filter.germ.comp_tendsto' {α : 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.comp_tendsto' g hg = f.lift_on (λ (f : α → β), filter.germ.map f g) _

source

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

↑f.comp_tendsto' g hg = filter.germ.map f g

source

def filter.germ.comp_tendsto {α : 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.comp_tendsto g hg = f.comp_tendsto' ↑g _

source

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

source

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

f.comp_tendsto' ↑g _ = f.comp_tendsto g hg

source

@[simp, norm_cast]

theorem filter.germ.const_inj {α : Type u_1} {β : Type u_2} {l : filter α} [l.ne_bot] {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_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (b : β) {lc : filter γ} {g : γ → α} (hg : filter.tendsto g lc l) :

↑b.comp_tendsto g hg = ↑b

source

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

↑b.comp_tendsto' g hg = ↑b

source

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

Prop

Lift a predicate on β to germ l β.

Equations

filter.germ.lift_pred p f = f.lift_on (λ (f : α → β), ∀ᶠ (x : α) in l, p (f x)) _

source

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

source

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

filter.germ.lift_pred p ↑x

source

@[simp]

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

filter.germ.lift_pred p ↑x ↔ p x

source

def filter.germ.lift_rel {α : 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.lift_rel r f g = quotient.lift_on₂' f g (λ (f : α → β) (g : α → γ), ∀ᶠ (x : α) in l, r (f x) (g x)) _

source

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

source

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

filter.germ.lift_rel r ↑x ↑y

source

@[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 : γ} :

filter.germ.lift_rel r ↑x ↑y ↔ r x y

source

@[protected, instance]

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

inhabited (l.germ β)

Equations

filter.germ.inhabited = {default := ↑inhabited.default}

source

@[protected, instance]

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

has_mul (l.germ M)

Equations

filter.germ.has_mul = {mul := filter.germ.map₂ has_mul.mul}

source

@[protected, instance]

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

has_add (l.germ M)

Equations

filter.germ.has_add = {add := filter.germ.map₂ has_add.add}

source

@[simp, norm_cast]

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

↑(f + g) = ↑f + ↑g

source

@[simp, norm_cast]

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

↑(f * g) = ↑f * ↑g

source

@[protected, instance]

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

has_zero (l.germ M)

Equations

filter.germ.has_zero = {zero := ↑0}

source

@[protected, instance]

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

has_one (l.germ M)

Equations

filter.germ.has_one = {one := ↑1}

source

@[simp, norm_cast]

theorem filter.germ.coe_zero {α : Type u_1} {l : filter α} {M : Type u_5} [has_zero M] :

↑0 = 0

source

@[simp, norm_cast]

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

↑1 = 1

source

@[protected, instance]

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

semigroup (l.germ M)

Equations

filter.germ.semigroup = function.surjective.semigroup coe filter.germ.semigroup._proof_1 filter.germ.semigroup._proof_2

source

@[protected, instance]

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

add_semigroup (l.germ M)

Equations

filter.germ.add_semigroup = function.surjective.add_semigroup coe filter.germ.add_semigroup._proof_1 filter.germ.add_semigroup._proof_2

source

@[protected, instance]

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

comm_semigroup (l.germ M)

Equations

filter.germ.comm_semigroup = function.surjective.comm_semigroup coe filter.germ.comm_semigroup._proof_1 filter.germ.comm_semigroup._proof_2

source

@[protected, instance]

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

add_comm_semigroup (l.germ M)

Equations

filter.germ.add_comm_semigroup = function.surjective.add_comm_semigroup coe filter.germ.add_comm_semigroup._proof_1 filter.germ.add_comm_semigroup._proof_2

source

@[protected, instance]

def filter.germ.left_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [left_cancel_semigroup M] :

left_cancel_semigroup (l.germ M)

Equations

filter.germ.left_cancel_semigroup = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, mul_left_cancel := _}

source

@[protected, instance]

def filter.germ.add_left_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [add_left_cancel_semigroup M] :

add_left_cancel_semigroup (l.germ M)

Equations

filter.germ.add_left_cancel_semigroup = {add := has_add.add filter.germ.has_add, add_assoc := _, add_left_cancel := _}

source

@[protected, instance]

def filter.germ.add_right_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [add_right_cancel_semigroup M] :

add_right_cancel_semigroup (l.germ M)

Equations

filter.germ.add_right_cancel_semigroup = {add := has_add.add filter.germ.has_add, add_assoc := _, add_right_cancel := _}

source

@[protected, instance]

def filter.germ.right_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [right_cancel_semigroup M] :

right_cancel_semigroup (l.germ M)

Equations

filter.germ.right_cancel_semigroup = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, mul_right_cancel := _}

source

@[protected, instance]

def filter.germ.has_vadd {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_vadd M G] :

has_vadd M (l.germ G)

Equations

filter.germ.has_vadd = {vadd := λ (n : M), filter.germ.map (has_vadd.vadd n)}

source

@[protected, instance]

def filter.germ.has_smul {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_smul M G] :

has_smul M (l.germ G)

Equations

filter.germ.has_smul = {smul := λ (n : M), filter.germ.map (has_smul.smul n)}

source

@[protected, instance]

def filter.germ.has_pow {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_pow G M] :

has_pow (l.germ G) M

Equations

filter.germ.has_pow = {pow := λ (f : l.germ G) (n : M), filter.germ.map (λ (_x : G), _x ^ n) f}

source

@[simp, norm_cast]

theorem filter.germ.coe_smul {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_smul M G] (n : M) (f : α → G) :

↑(n • f) = n • ↑f

source

@[simp, norm_cast]

theorem filter.germ.coe_vadd {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_vadd M G] (n : M) (f : α → G) :

↑(n +ᵥ f) = n +ᵥ ↑f

source

@[simp, norm_cast]

theorem filter.germ.const_smul {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_smul M G] (n : M) (a : G) :

↑(n • a) = n • ↑a

source

@[simp, norm_cast]

theorem filter.germ.const_vadd {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_vadd M G] (n : M) (a : G) :

↑(n +ᵥ a) = n +ᵥ ↑a

source

@[simp, norm_cast]

theorem filter.germ.coe_pow {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_pow G M] (f : α → G) (n : M) :

↑(f ^ n) = ↑f ^ n

source

@[simp, norm_cast]

theorem filter.germ.const_pow {α : Type u_1} {l : filter α} {M : Type u_5} {G : Type u_6} [has_pow G M] (a : G) (n : M) :

↑(a ^ n) = ↑a ^ n

source

@[protected, instance]

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

add_monoid (l.germ M)

Equations

filter.germ.add_monoid = function.surjective.add_monoid coe filter.germ.add_monoid._proof_1 filter.germ.add_monoid._proof_2 filter.germ.add_monoid._proof_3 filter.germ.add_monoid._proof_4

source

@[protected, instance]

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

monoid (l.germ M)

Equations

filter.germ.monoid = function.surjective.monoid coe filter.germ.monoid._proof_1 filter.germ.monoid._proof_2 filter.germ.monoid._proof_3 filter.germ.monoid._proof_4

source

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.

Equations

filter.germ.coe_add_hom l = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

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

filter.germ.coe_mul_hom l = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}

source

@[simp]

theorem filter.germ.coe_coe_add_hom {α : Type u_1} {l : filter α} {M : Type u_5} [add_monoid M] :

⇑(filter.germ.coe_add_hom l) = coe

source

@[simp]

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

⇑(filter.germ.coe_mul_hom l) = coe

source

@[protected, instance]

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

comm_monoid (l.germ M)

Equations

filter.germ.comm_monoid = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow filter.germ.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

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

add_comm_monoid (l.germ M)

Equations

filter.germ.add_comm_monoid = {add := has_add.add filter.germ.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul filter.germ.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def filter.germ.add_monoid_with_one {α : Type u_1} {l : filter α} {M : Type u_5} [add_monoid_with_one M] :

add_monoid_with_one (l.germ M)

Equations

filter.germ.add_monoid_with_one = {nat_cast := λ (n : ℕ), ↑↑n, add := add_monoid.add filter.germ.add_monoid, add_assoc := _, zero := add_monoid.zero filter.germ.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul filter.germ.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}

source

@[protected, instance]

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

has_inv (l.germ G)

Equations

filter.germ.has_inv = {inv := filter.germ.map has_inv.inv}

source

@[protected, instance]

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

has_neg (l.germ G)

Equations

filter.germ.has_neg = {neg := filter.germ.map has_neg.neg}

source

@[simp, norm_cast]

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

↑-f = -↑f

source

@[simp, norm_cast]

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

↑f⁻¹ = (↑f)⁻¹

source

@[simp, norm_cast]

theorem filter.germ.const_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] (a : G) :

↑-a = -↑a

source

@[simp, norm_cast]

theorem filter.germ.const_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] (a : G) :

↑a⁻¹ = (↑a)⁻¹

source

@[protected, instance]

def filter.germ.has_sub {α : Type u_1} {l : filter α} {M : Type u_5} [has_sub M] :

has_sub (l.germ M)

Equations

filter.germ.has_sub = {sub := filter.germ.map₂ has_sub.sub}

source

@[protected, instance]

def filter.germ.has_div {α : Type u_1} {l : filter α} {M : Type u_5} [has_div M] :

has_div (l.germ M)

Equations

filter.germ.has_div = {div := filter.germ.map₂ has_div.div}

source

@[simp, norm_cast]

theorem filter.germ.coe_div {α : Type u_1} {l : filter α} {M : Type u_5} [has_div M] (f g : α → M) :

↑(f / g) = ↑f / ↑g

source

@[simp, norm_cast]

theorem filter.germ.coe_sub {α : Type u_1} {l : filter α} {M : Type u_5} [has_sub M] (f g : α → M) :

↑(f - g) = ↑f - ↑g

source

@[simp, norm_cast]

theorem filter.germ.const_sub {α : Type u_1} {l : filter α} {M : Type u_5} [has_sub M] (a b : M) :

↑(a - b) = ↑a - ↑b

source

@[simp, norm_cast]

theorem filter.germ.const_div {α : Type u_1} {l : filter α} {M : Type u_5} [has_div M] (a b : M) :

↑(a / b) = ↑a / ↑b

source

@[protected, instance]

def filter.germ.sub_neg_monoid {α : Type u_1} {l : filter α} {G : Type u_6} [sub_neg_monoid G] :

sub_neg_monoid (l.germ G)

Equations

filter.germ.sub_neg_monoid = function.surjective.sub_neg_monoid coe filter.germ.sub_neg_monoid._proof_1 filter.germ.sub_neg_monoid._proof_2 filter.germ.sub_neg_monoid._proof_3 filter.germ.sub_neg_monoid._proof_4 filter.germ.sub_neg_monoid._proof_5 filter.germ.sub_neg_monoid._proof_6 filter.germ.sub_neg_monoid._proof_7

source

@[protected, instance]

def filter.germ.div_inv_monoid {α : Type u_1} {l : filter α} {G : Type u_6} [div_inv_monoid G] :

div_inv_monoid (l.germ G)

Equations

filter.germ.div_inv_monoid = function.surjective.div_inv_monoid coe filter.germ.div_inv_monoid._proof_1 filter.germ.div_inv_monoid._proof_2 filter.germ.div_inv_monoid._proof_3 filter.germ.div_inv_monoid._proof_4 filter.germ.div_inv_monoid._proof_5 filter.germ.div_inv_monoid._proof_6 filter.germ.div_inv_monoid._proof_7

source

@[protected, instance]

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

group (l.germ G)

Equations

filter.germ.group = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := div_inv_monoid.npow filter.germ.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv filter.germ.div_inv_monoid, div := div_inv_monoid.div filter.germ.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow filter.germ.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

@[protected, instance]

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

add_group (l.germ G)

Equations

filter.germ.add_group = {add := has_add.add filter.germ.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul filter.germ.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg filter.germ.sub_neg_monoid, sub := sub_neg_monoid.sub filter.germ.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul filter.germ.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}

source

@[protected, instance]

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

add_comm_group (l.germ G)

Equations

filter.germ.add_comm_group = {add := has_add.add filter.germ.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_group.nsmul filter.germ.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg filter.germ.has_neg, sub := add_group.sub filter.germ.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul filter.germ.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected, instance]

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

comm_group (l.germ G)

Equations

filter.germ.comm_group = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := group.npow filter.germ.group, npow_zero' := _, npow_succ' := _, inv := has_inv.inv filter.germ.has_inv, div := group.div filter.germ.group, div_eq_mul_inv := _, zpow := group.zpow filter.germ.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

@[protected, instance]

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

nontrivial (l.germ R)

source

@[protected, instance]

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

mul_zero_class (l.germ R)

Equations

filter.germ.mul_zero_class = {mul := has_mul.mul filter.germ.has_mul, zero := 0, zero_mul := _, mul_zero := _}

source

@[protected, instance]

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

distrib (l.germ R)

Equations

filter.germ.distrib = {mul := has_mul.mul filter.germ.has_mul, add := has_add.add filter.germ.has_add, left_distrib := _, right_distrib := _}

source

@[protected, instance]

def filter.germ.semiring {α : Type u_1} {l : filter α} {R : Type u_5} [semiring R] :

semiring (l.germ R)

Equations

filter.germ.semiring = {add := add_comm_monoid.add filter.germ.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero filter.germ.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul filter.germ.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul filter.germ.monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one filter.germ.monoid, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast filter.germ.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow filter.germ.monoid, npow_zero' := _, npow_succ' := _}

source

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

filter.germ.coe_ring_hom l = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

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

⇑(filter.germ.coe_ring_hom l) = coe

source

@[protected, instance]

def filter.germ.ring {α : Type u_1} {l : filter α} {R : Type u_5} [ring R] :

ring (l.germ R)

Equations

filter.germ.ring = {add := add_comm_group.add filter.germ.add_comm_group, add_assoc := _, zero := add_comm_group.zero filter.germ.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul filter.germ.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg filter.germ.add_comm_group, sub := add_comm_group.sub filter.germ.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul filter.germ.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast add_comm_group.add filter.germ.ring._proof_12 add_comm_group.zero filter.germ.ring._proof_13 filter.germ.ring._proof_14 add_comm_group.nsmul filter.germ.ring._proof_15 filter.germ.ring._proof_16 semiring.one filter.germ.ring._proof_17 filter.germ.ring._proof_18 add_comm_group.neg add_comm_group.sub filter.germ.ring._proof_19 add_comm_group.zsmul filter.germ.ring._proof_20 filter.germ.ring._proof_21 filter.germ.ring._proof_22 filter.germ.ring._proof_23, nat_cast := semiring.nat_cast filter.germ.semiring, one := semiring.one filter.germ.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul filter.germ.semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow filter.germ.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

source

@[protected, instance]

def filter.germ.comm_semiring {α : Type u_1} {l : filter α} {R : Type u_5} [comm_semiring R] :

comm_semiring (l.germ R)

Equations

filter.germ.comm_semiring = {add := semiring.add filter.germ.semiring, add_assoc := _, zero := semiring.zero filter.germ.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul filter.germ.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul filter.germ.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one filter.germ.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast filter.germ.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow filter.germ.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def filter.germ.comm_ring {α : Type u_1} {l : filter α} {R : Type u_5} [comm_ring R] :

comm_ring (l.germ R)

Equations

filter.germ.comm_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[protected, instance]

def filter.germ.has_smul' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_smul M β] :

has_smul (l.germ M) (l.germ β)

Equations

filter.germ.has_smul' = {smul := filter.germ.map₂ has_smul.smul}

source

@[protected, instance]

def filter.germ.has_vadd' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_vadd M β] :

has_vadd (l.germ M) (l.germ β)

Equations

filter.germ.has_vadd' = {vadd := filter.germ.map₂ has_vadd.vadd}

source

@[simp, norm_cast]

theorem filter.germ.coe_smul' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_smul M β] (c : α → M) (f : α → β) :

↑(c • f) = ↑c • ↑f

source

@[simp, norm_cast]

theorem filter.germ.coe_vadd' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [has_vadd M β] (c : α → M) (f : α → β) :

↑(c +ᵥ f) = ↑c +ᵥ ↑f

source

@[protected, instance]

def filter.germ.add_action {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [add_monoid M] [add_action M β] :

add_action M (l.germ β)

Equations

filter.germ.add_action = {to_has_vadd := filter.germ.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}

source

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

filter.germ.mul_action = {to_has_smul := filter.germ.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}

source

@[protected, instance]

def filter.germ.add_action' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [add_monoid M] [add_action M β] :

add_action (l.germ M) (l.germ β)

Equations

filter.germ.add_action' = {to_has_vadd := filter.germ.has_vadd' add_action.to_has_vadd, zero_vadd := _, add_vadd := _}

source

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

filter.germ.mul_action' = {to_has_smul := filter.germ.has_smul' mul_action.to_has_smul, one_smul := _, mul_smul := _}

source

@[protected, instance]

def filter.germ.distrib_mul_action {α : Type u_1} {l : filter α} {M : Type u_5} {N : Type u_6} [monoid M] [add_monoid N] [distrib_mul_action M N] :

distrib_mul_action M (l.germ N)

Equations

filter.germ.distrib_mul_action = {to_mul_action := filter.germ.mul_action distrib_mul_action.to_mul_action, smul_zero := _, smul_add := _}

source

@[protected, instance]

def filter.germ.distrib_mul_action' {α : Type u_1} {l : filter α} {M : Type u_5} {N : Type u_6} [monoid M] [add_monoid N] [distrib_mul_action M N] :

distrib_mul_action (l.germ M) (l.germ N)

Equations

filter.germ.distrib_mul_action' = {to_mul_action := filter.germ.mul_action' distrib_mul_action.to_mul_action, smul_zero := _, smul_add := _}

source

@[protected, instance]

def filter.germ.module {α : Type u_1} {l : filter α} {M : Type u_5} {R : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :

module R (l.germ M)

Equations

filter.germ.module = {to_distrib_mul_action := filter.germ.distrib_mul_action module.to_distrib_mul_action, add_smul := _, zero_smul := _}

source

@[protected, instance]

def filter.germ.module' {α : Type u_1} {l : filter α} {M : Type u_5} {R : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :

module (l.germ R) (l.germ M)

Equations

filter.germ.module' = {to_distrib_mul_action := filter.germ.distrib_mul_action' module.to_distrib_mul_action, add_smul := _, zero_smul := _}

source

@[protected, instance]

def filter.germ.has_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :

has_le (l.germ β)

Equations

filter.germ.has_le = {le := filter.germ.lift_rel has_le.le}

source

theorem filter.germ.le_def {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :

has_le.le = filter.germ.lift_rel has_le.le

source

@[simp]

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

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

source

theorem filter.germ.coe_nonneg {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [has_zero β] {f : α → β} :

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

source

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

x ≤ y → ↑x ≤ ↑y

source

@[simp, norm_cast]

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

source

@[protected, instance]

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

preorder (l.germ β)

Equations

filter.germ.preorder = {le := has_le.le filter.germ.has_le, lt := λ (a b : l.germ β), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[protected, instance]

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

partial_order (l.germ β)

Equations

filter.germ.partial_order = {le := has_le.le filter.germ.has_le, lt := preorder.lt filter.germ.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def filter.germ.has_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :

has_bot (l.germ β)

Equations

filter.germ.has_bot = {bot := ↑⊥}

source

@[protected, instance]

def filter.germ.has_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :

has_top (l.germ β)

Equations

filter.germ.has_top = {top := ↑⊤}

source

@[simp, norm_cast]

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

↑⊥ = ⊥

source

@[simp, norm_cast]

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

↑⊤ = ⊤

source

@[protected, instance]

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

order_bot (l.germ β)

Equations

filter.germ.order_bot = {bot := ⊥, bot_le := _}

source

@[protected, instance]

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

order_top (l.germ β)

Equations

filter.germ.order_top = {top := ⊤, le_top := _}

source

@[protected, instance]

def filter.germ.bounded_order {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [bounded_order β] :

bounded_order (l.germ β)

Equations

filter.germ.bounded_order = {top := order_top.top filter.germ.order_top, le_top := _, bot := order_bot.bot filter.germ.order_bot, bot_le := _}