mathlib3 documentation

order.filter.germ

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

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

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 γ} (hg : filter.tendsto g lc l) :
f 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} (l : filter α) (β : Type u_2) :
Type (max u_1 u_2)

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

Equations
Instances for filter.germ
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
Instances for filter.product_setoid
@[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
Instances for filter.product
@[protected, instance]
def filter.product.has_coe_t {α : Type u_1} {l : filter α} {ε : α Type u_5} :
has_coe_t (Π (a : α), ε a) (l.product ε)
Equations
@[protected, instance]
def filter.product.inhabited {α : Type u_1} {l : filter α} {ε : α Type u_5} [Π (a : α), inhabited (ε a)] :
Equations
@[protected, instance]
def filter.germ.has_coe_t {α : Type u_1} {β : Type u_2} {l : filter α} :
has_coe_t β) (l.germ β)
Equations
@[protected, 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} (h : (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} (h : (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} (H : (f : α β) (g : α γ) (h : α δ), p f g h) :
p f g h
def filter.germ.map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : filter α} {lc : filter γ} (F : β) γ δ) (hF : (l.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
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
@[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, norm_cast]
theorem filter.germ.coe_eq {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α β} :
f = g f =ᶠ[l] g
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.

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
@[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 α} (op : β γ δ) :
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))
@[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
@[simp, norm_cast]
theorem filter.germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {lb : filter β} :
theorem filter.tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {lb : filter β} :

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

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
@[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 : γ α) (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
@[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, norm_cast]
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 α} (p : β Prop) (f : 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 : β} (hx : p 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 α} (r : β γ Prop) (f : l.germ β) (g : 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 : γ} (h : r 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 : γ} :
@[protected, instance]
def filter.germ.inhabited {α : Type u_1} {β : Type u_2} {l : filter α} [inhabited β] :
Equations
@[protected, instance]
def filter.germ.has_mul {α : Type u_1} {l : filter α} {M : Type u_5} [has_mul M] :
Equations
@[protected, instance]
def filter.germ.has_add {α : Type u_1} {l : filter α} {M : Type u_5} [has_add M] :
Equations
@[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
@[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
@[protected, instance]
def filter.germ.has_zero {α : Type u_1} {l : filter α} {M : Type u_5} [has_zero M] :
Equations
@[protected, instance]
def filter.germ.has_one {α : Type u_1} {l : filter α} {M : Type u_5} [has_one M] :
Equations
@[simp, norm_cast]
theorem filter.germ.coe_zero {α : Type u_1} {l : filter α} {M : Type u_5} [has_zero M] :
0 = 0
@[simp, norm_cast]
theorem filter.germ.coe_one {α : Type u_1} {l : filter α} {M : Type u_5} [has_one M] :
1 = 1
@[protected, instance]
def filter.germ.semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [semigroup M] :
Equations
@[protected, instance]
def filter.germ.add_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [add_semigroup M] :
Equations
@[protected, instance]
def filter.germ.comm_semigroup {α : Type u_1} {l : filter α} {M : Type u_5} [comm_semigroup M] :
Equations
@[protected, instance]
Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[protected, instance]
def filter.germ.add_monoid {α : Type u_1} {l : filter α} {M : Type u_5} [add_monoid M] :
Equations
@[protected, 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.

Equations
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] :
@[protected, instance]
def filter.germ.comm_monoid {α : Type u_1} {l : filter α} {M : Type u_5} [comm_monoid M] :
Equations
@[protected, instance]
def filter.germ.has_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] :
Equations
@[protected, instance]
def filter.germ.has_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] :
Equations
@[simp, norm_cast]
theorem filter.germ.coe_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] (f : α G) :
@[simp, norm_cast]
theorem filter.germ.coe_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] (f : α G) :
@[simp, norm_cast]
theorem filter.germ.const_neg {α : Type u_1} {l : filter α} {G : Type u_6} [has_neg G] (a : G) :
@[simp, norm_cast]
theorem filter.germ.const_inv {α : Type u_1} {l : filter α} {G : Type u_6} [has_inv G] (a : G) :
@[protected, instance]
def filter.germ.has_sub {α : Type u_1} {l : filter α} {M : Type u_5} [has_sub M] :
Equations
@[protected, instance]
def filter.germ.has_div {α : Type u_1} {l : filter α} {M : Type u_5} [has_div M] :
Equations
@[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
@[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
@[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
@[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
@[protected, instance]
def filter.germ.sub_neg_monoid {α : Type u_1} {l : filter α} {G : Type u_6} [sub_neg_monoid 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
@[protected, instance]
def filter.germ.div_inv_monoid {α : Type u_1} {l : filter α} {G : Type u_6} [div_inv_monoid 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
@[protected, instance]
def filter.germ.nontrivial {α : Type u_1} {l : filter α} {R : Type u_5} [nontrivial R] [l.ne_bot] :
@[protected, instance]
def filter.germ.mul_zero_class {α : Type u_1} {l : filter α} {R : Type u_5} [mul_zero_class R] :
Equations
@[protected, 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] :
@[protected, instance]
def filter.germ.ring {α : Type u_1} {l : filter α} {R : Type u_5} [ring R] :
ring (l.germ R)
Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[protected, instance]
def filter.germ.has_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :
has_le (l.germ β)
Equations
theorem filter.germ.le_def {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :
@[simp]
theorem filter.germ.coe_le {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α β} [has_le β] :
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
theorem filter.germ.const_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] {x y : β} :
x y x y
@[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
@[protected, instance]
def filter.germ.preorder {α : Type u_1} {β : Type u_2} {l : filter α} [preorder β] :
preorder (l.germ β)
Equations
@[protected, instance]
def filter.germ.has_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :
has_bot (l.germ β)
Equations
@[protected, instance]
def filter.germ.has_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :
has_top (l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.const_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :
@[simp, norm_cast]
theorem filter.germ.const_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :
@[protected, instance]
def filter.germ.order_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [order_bot β] :
Equations
@[protected, instance]
def filter.germ.order_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [order_top β] :
Equations