# mathlibdocumentation

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

• 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

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 : 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
• = {r := λ (f g : Π (a : α), ε a), ∀ᶠ (a : α) in l, f a = g a, iseqv := _}
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 α} :
(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
• hF = hF
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 : α → β) :
hF 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] gf = 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 : α → β) :
f = (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₂ 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 : α → γ) :
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 β} :
f.tendsto lb lb
theorem filter.tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {lb : filter β} :
lbf.tendsto lb

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
• hg = f.lift_on (λ (f : α → β), g) _
@[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) :
hg =
def filter.germ.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (f : l.germ β) {lc : filter γ} (g : γ → α) (hg : 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 : lc l) :
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 : lc l) :
_ = f.comp_tendsto g hg
@[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 : β → γ) :
= (f a)
@[simp]
theorem filter.germ.map₂_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : filter α) (b : β) (c : γ) (f : β → γ → δ) :
c = (f b c)
@[simp]
theorem filter.germ.const_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} (b : β) {lc : filter γ} {g : γ → α} (hg : lc l) :
hg = b
@[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) :
hg = b
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
• = f.lift_on (λ (f : α → β), ∀ᶠ (x : α) in l, p (f x)) _
@[simp]
theorem filter.germ.lift_pred_coe {α : Type u_1} {β : Type u_2} {l : filter α} {p : β → Prop} {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 : β} :
p 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
• g = (λ (f : α → β) (g : α → γ), ∀ᶠ (x : α) in l, r (f x) (g x)) _
@[simp]
theorem filter.germ.lift_rel_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : filter α} {r : β → γ → Prop} {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 : γ} :
r 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}  :
Equations
@[protected, instance]
def filter.germ.comm_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.add_comm_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.left_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.add_left_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.add_right_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.right_cancel_semigroup {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.has_nat_pow {α : Type u_1} {l : filter α} {G : Type u_6} [monoid G] :
Equations
@[simp]
theorem filter.germ.coe_pow {α : Type u_1} {l : filter α} {G : Type u_6} [monoid G] (f : α → G) (n : ) :
(f ^ n) = f ^ n
@[protected, instance]
def filter.germ.has_int_pow {α : Type u_1} {l : filter α} {G : Type u_6}  :
Equations
@[simp]
theorem filter.germ.coe_zpow {α : Type u_1} {l : filter α} {G : Type u_6} (f : α → G) (z : ) :
(f ^ z) = f ^ z
@[protected, instance]
def filter.germ.has_smul {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [ β] :
(l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.coe_smul {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [ β] (c : M) (f : α → β) :
(c f) = c f
@[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.add_comm_monoid {α : Type u_1} {l : filter α} {M : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.add_monoid_with_one {α : Type u_1} {l : filter α} {M : Type u_5}  :
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) :
@[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
@[protected, instance]
def filter.germ.sub_neg_monoid {α : Type u_1} {l : filter α} {G : Type u_6}  :
Equations
• filter.germ.sub_neg_monoid = 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}  :
Equations
• filter.germ.div_inv_monoid = 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.group {α : Type u_1} {l : filter α} {G : Type u_6} [group G] :
group (l.germ G)
Equations
@[protected, instance]
def filter.germ.add_group {α : Type u_1} {l : filter α} {G : Type u_6} [add_group G] :
Equations
@[protected, instance]
def filter.germ.add_comm_group {α : Type u_1} {l : filter α} {G : Type u_6}  :
Equations
@[protected, instance]
def filter.germ.comm_group {α : Type u_1} {l : filter α} {G : Type u_6} [comm_group G] :
Equations
@[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}  :
Equations
@[protected, instance]
def filter.germ.distrib {α : Type u_1} {l : filter α} {R : Type u_5} [distrib R] :
Equations
@[protected, instance]
def filter.germ.semiring {α : Type u_1} {l : filter α} {R : Type u_5} [semiring 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.comm_semiring {α : Type u_1} {l : filter α} {R : Type u_5}  :
Equations
@[protected, instance]
def filter.germ.comm_ring {α : Type u_1} {l : filter α} {R : Type u_5} [comm_ring R] :
Equations
@[protected, instance]
def filter.germ.has_smul' {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [ β] :
has_smul (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} [ β] (c : α → M) (f : α → β) :
(c f) = c f
@[protected, instance]
def filter.germ.mul_action {α : Type u_1} {β : Type u_2} {l : filter α} {M : Type u_5} [monoid 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 (l.germ M) (l.germ β)
Equations
@[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] [ N] :
(l.germ N)
Equations
@[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] [ N] :
Equations
@[protected, instance]
def filter.germ.module {α : Type u_1} {l : filter α} {M : Type u_5} {R : Type u_7} [semiring R] [ M] :
(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] [ 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
@[simp]
theorem filter.germ.coe_le {α : Type u_1} {β : Type u_2} {l : filter α} {f g : α → β} [has_le β] :
theorem filter.germ.le_def {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] :
theorem filter.germ.const_le {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] {x y : β} (h : 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.partial_order {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.has_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :
has_bot (l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.const_bot {α : Type u_1} {β : Type u_2} {l : filter α} [has_bot β] :
@[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.has_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :
has_top (l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.const_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_top β] :
@[protected, instance]
def filter.germ.order_top {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β] [order_top β] :
Equations
@[protected, instance]
def filter.germ.has_sup {α : Type u_1} {β : Type u_2} {l : filter α} [has_sup β] :
has_sup (l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.const_sup {α : Type u_1} {β : Type u_2} {l : filter α} [has_sup β] (a b : β) :
(a b) = a b
@[protected, instance]
def filter.germ.has_inf {α : Type u_1} {β : Type u_2} {l : filter α} [has_inf β] :
has_inf (l.germ β)
Equations
@[simp, norm_cast]
theorem filter.germ.const_inf {α : Type u_1} {β : Type u_2} {l : filter α} [has_inf β] (a b : β) :
(a b) = a b
@[protected, instance]
def filter.germ.semilattice_sup {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.semilattice_inf {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.lattice {α : Type u_1} {β : Type u_2} {l : filter α} [lattice β] :
lattice (l.germ β)
Equations
@[protected, instance]
def filter.germ.bounded_order {α : Type u_1} {β : Type u_2} {l : filter α} [has_le β]  :
Equations
@[protected, instance]
def filter.germ.ordered_cancel_comm_monoid {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_cancel_add_comm_monoid {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_comm_group {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations
@[protected, instance]
def filter.germ.ordered_add_comm_group {α : Type u_1} {β : Type u_2} {l : filter α}  :
Equations