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

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 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. 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, semimodule;
preorder, partial_order, and lattice structures up to bounded_lattice;
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 γ} :

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} :

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

source

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

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

(∀ (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} :

(∀ (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} :

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

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

(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]

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

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

source

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

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 α} :

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

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

f.tendsto lb = f.lift_on (λ (f : α → β), filter.tendsto f l lb) _

source

@[simp]

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

↑f.tendsto lb ↔ filter.tendsto f l lb

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 α) :

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

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]

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 α} :

(β → Prop) → 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 : β} :

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 α} :

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

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

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

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

@[instance]

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

has_add (l.germ M)

source

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

source

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

source

@[instance]

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

has_zero (l.germ M)

source

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

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

↑0 = 0

source

@[simp]

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

↑1 = 1

source

@[instance]

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

semigroup (l.germ M)

Equations

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

source

@[instance]

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

add_semigroup (l.germ M)

source

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

source

@[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 = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, mul_comm := _}

source

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

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

source

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

source

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

@[instance]

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

monoid (l.germ M)

Equations

filter.germ.monoid = {mul := has_mul.mul filter.germ.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}

source

@[instance]

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

add_monoid (l.germ M)

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.

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

@[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 := _, mul_comm := _}

source

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

source

@[instance]

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

has_neg (l.germ G)

source

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

@[simp]

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

↑-f = -↑f

source

@[simp]

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

↑f⁻¹ = (↑f)⁻¹

source

@[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 := _, inv := has_inv.inv filter.germ.has_inv, mul_left_inv := _}

source

@[instance]

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

add_group (l.germ G)

source

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

source

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

source

@[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 := _, inv := has_inv.inv filter.germ.has_inv, mul_left_inv := _, mul_comm := _}

source

@[instance]

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

nontrivial (l.germ R)

Equations

filter.germ.nontrivial = _
_ = _

source

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

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

@[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 := _, add_comm := _, mul := monoid.mul filter.germ.monoid, mul_assoc := _, one := monoid.one filter.germ.monoid, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

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

@[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 := _, neg := add_comm_group.neg filter.germ.add_comm_group, add_left_neg := _, add_comm := _, mul := monoid.mul filter.germ.monoid, mul_assoc := _, one := monoid.one filter.germ.monoid, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

source

@[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 := _, add_comm := _, mul := semiring.mul filter.germ.semiring, mul_assoc := _, one := semiring.one filter.germ.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[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 := _, neg := ring.neg filter.germ.ring, add_left_neg := _, add_comm := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one := ring.one filter.germ.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

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

filter.germ.has_scalar = {smul := λ (c : M), filter.germ.map (has_scalar.smul c)}

source

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

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

source

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

source

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

source

@[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_scalar := filter.germ.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}

source

@[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_scalar := filter.germ.has_scalar' mul_action.to_has_scalar, one_smul := _, mul_smul := _}

source

@[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_add := _, smul_zero := _}

source

@[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_add := _, smul_zero := _}

source

@[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 R (l.germ M)

Equations

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

source

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

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

source

@[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 := λ (f g : l.germ β), quotient.lift_on₂' f g l.eventually_le filter.germ.has_le._proof_1}

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.const_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] {x y : β} :

x ≤ y → ↑x ≤ ↑y

source

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

source

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

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

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

@[simp]

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

↑⊥ = ⊥

source

@[instance]

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

order_bot (l.germ β)

Equations

filter.germ.order_bot = {bot := ⊥, le := has_le.le filter.germ.has_le, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

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

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

↑⊤ = ⊤

source

@[instance]

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

order_top (l.germ β)

Equations

filter.germ.order_top = {top := ⊤, le := has_le.le filter.germ.has_le, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[instance]

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

has_sup (l.germ β)

Equations

filter.germ.has_sup = {sup := filter.germ.map₂ has_sup.sup}

source

@[simp]

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

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

source

@[instance]

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

has_inf (l.germ β)

Equations

filter.germ.has_inf = {inf := filter.germ.map₂ has_inf.inf}

source

@[simp]

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

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

source

@[instance]

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

semilattice_sup (l.germ β)

Equations

filter.germ.semilattice_sup = {sup := has_sup.sup filter.germ.has_sup, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

semilattice_inf (l.germ β)

Equations

filter.germ.semilattice_inf = {inf := has_inf.inf filter.germ.has_inf, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_inf_bot (l.germ β)

Equations

filter.germ.semilattice_inf_bot = {bot := order_bot.bot filter.germ.order_bot, le := semilattice_inf.le filter.germ.semilattice_inf, lt := semilattice_inf.lt filter.germ.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf filter.germ.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_sup_bot (l.germ β)

Equations

filter.germ.semilattice_sup_bot = {bot := order_bot.bot filter.germ.order_bot, le := semilattice_sup.le filter.germ.semilattice_sup, lt := semilattice_sup.lt filter.germ.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup filter.germ.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

semilattice_inf_top (l.germ β)

Equations

filter.germ.semilattice_inf_top = {top := order_top.top filter.germ.order_top, le := semilattice_inf.le filter.germ.semilattice_inf, lt := semilattice_inf.lt filter.germ.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf filter.germ.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_sup_top (l.germ β)

Equations

filter.germ.semilattice_sup_top = {top := order_top.top filter.germ.order_top, le := semilattice_sup.le filter.germ.semilattice_sup, lt := semilattice_sup.lt filter.germ.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup filter.germ.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

lattice (l.germ β)

Equations

filter.germ.lattice = {sup := semilattice_sup.sup filter.germ.semilattice_sup, le := semilattice_sup.le filter.germ.semilattice_sup, lt := semilattice_sup.lt filter.germ.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf filter.germ.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

bounded_lattice (l.germ β)

Equations

filter.germ.bounded_lattice = {sup := lattice.sup filter.germ.lattice, le := lattice.le filter.germ.lattice, lt := lattice.lt filter.germ.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf filter.germ.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top filter.germ.order_top, le_top := _, bot := order_bot.bot filter.germ.order_bot, bot_le := _}

source

@[instance]

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

ordered_cancel_comm_monoid (l.germ β)

Equations

filter.germ.ordered_cancel_comm_monoid = {mul := comm_monoid.mul filter.germ.comm_monoid, mul_assoc := _, one := comm_monoid.one filter.germ.comm_monoid, one_mul := _, mul_one := _, mul_comm := _, mul_left_cancel := _, mul_right_cancel := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

@[instance]

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

ordered_cancel_add_comm_monoid (l.germ β)

source

@[instance]

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

ordered_add_comm_group (l.germ β)

source

@[instance]

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

ordered_comm_group (l.germ β)

Equations

filter.germ.ordered_comm_group = {mul := comm_group.mul filter.germ.comm_group, mul_assoc := _, one := comm_group.one filter.germ.comm_group, one_mul := _, mul_one := _, inv := comm_group.inv filter.germ.comm_group, mul_left_inv := _, mul_comm := _, le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

mathlib documentation

order.filter.germ

Germ of a function at a filter

Main definitions

Tags

General documentation

Additional documentation

Library

mathlib documentation

order.​filter.​germ

Germ of a function at a filter

Main definitions

Tags

General documentation

Additional documentation

Library

order.filter.germ