# mathlib3documentation

topology.algebra.order.field

# Topologies on linear ordered fields #

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

theorem mul_tendsto_nhds_zero_right {α : Type u_1} (x : α) :
((nhds 0).prod (nhds x)) (nhds 0)
theorem mul_tendsto_nhds_zero_left {α : Type u_1} (x : α) :
((nhds x).prod (nhds 0)) (nhds 0)
theorem nhds_eq_map_mul_left_nhds_one {α : Type u_1} {x₀ : α} (hx₀ : x₀ 0) :
nhds x₀ = filter.map (λ (x : α), x₀ * x) (nhds 1)
theorem nhds_eq_map_mul_right_nhds_one {α : Type u_1} {x₀ : α} (hx₀ : x₀ 0) :
nhds x₀ = filter.map (λ (x : α), x * x₀) (nhds 1)
theorem mul_tendsto_nhds_one_nhds_one {α : Type u_1}  :
((nhds 1).prod (nhds 1)) (nhds 1)
@[protected, instance]
theorem filter.tendsto.at_top_mul {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : 0 < C) (hf : filter.at_top) (hg : (nhds C)) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to at_top and g tends to a positive constant C then f * g tends to at_top.

theorem filter.tendsto.mul_at_top {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : 0 < C) (hf : (nhds C)) (hg : filter.at_top) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to a positive constant C and g tends to at_top then f * g tends to at_top.

theorem filter.tendsto.at_top_mul_neg {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : C < 0) (hf : filter.at_top) (hg : (nhds C)) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to at_top and g tends to a negative constant C then f * g tends to at_bot.

theorem filter.tendsto.neg_mul_at_top {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : C < 0) (hf : (nhds C)) (hg : filter.at_top) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to a negative constant C and g tends to at_top then f * g tends to at_bot.

theorem filter.tendsto.at_bot_mul {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : 0 < C) (hf : filter.at_bot) (hg : (nhds C)) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to at_bot and g tends to a positive constant C then f * g tends to at_bot.

theorem filter.tendsto.at_bot_mul_neg {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : C < 0) (hf : filter.at_bot) (hg : (nhds C)) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to at_bot and g tends to a negative constant C then f * g tends to at_top.

theorem filter.tendsto.mul_at_bot {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : 0 < C) (hf : (nhds C)) (hg : filter.at_bot) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to a positive constant C and g tends to at_bot then f * g tends to at_bot.

theorem filter.tendsto.neg_mul_at_bot {α : Type u_1} {β : Type u_2} {l : filter β} {f g : β α} {C : α} (hC : C < 0) (hf : (nhds C)) (hg : filter.at_bot) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to a negative constant C and g tends to at_bot then f * g tends to at_top.

theorem tendsto_inv_zero_at_top {α : Type u_1}  :

The function x ↦ x⁻¹ tends to +∞ on the right of 0.

theorem tendsto_inv_at_top_zero' {α : Type u_1}  :

The function r ↦ r⁻¹ tends to 0 on the right as r → +∞.

theorem tendsto_inv_at_top_zero {α : Type u_1}  :
theorem filter.tendsto.div_at_top {α : Type u_1} {β : Type u_2} {f g : β α} {l : filter β} {a : α} (h : (nhds a)) (hg : filter.at_top) :
filter.tendsto (λ (x : β), f x / g x) l (nhds 0)
theorem filter.tendsto.inv_tendsto_at_top {α : Type u_1} {β : Type u_2} {l : filter β} {f : β α} (h : filter.at_top) :
(nhds 0)
theorem filter.tendsto.inv_tendsto_zero {α : Type u_1} {β : Type u_2} {l : filter β} {f : β α} (h : (set.Ioi 0))) :
theorem tendsto_pow_neg_at_top {α : Type u_1} {n : } (hn : n 0) :
filter.tendsto (λ (x : α), x ^ -n) filter.at_top (nhds 0)

The function x^(-n) tends to 0 at +∞ for any positive natural n. A version for positive real powers exists as tendsto_rpow_neg_at_top.

theorem tendsto_zpow_at_top_zero {α : Type u_1} {n : } (hn : n < 0) :
filter.tendsto (λ (x : α), x ^ n) filter.at_top (nhds 0)
theorem tendsto_const_mul_zpow_at_top_zero {α : Type u_1} {n : } {c : α} (hn : n < 0) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top (nhds 0)
theorem tendsto_const_mul_pow_nhds_iff' {α : Type u_1} {n : } {c d : α} :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top (nhds d) (c = 0 n = 0) c = d
theorem tendsto_const_mul_pow_nhds_iff {α : Type u_1} {n : } {c d : α} (hc : c 0) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top (nhds d) n = 0 c = d
theorem tendsto_const_mul_zpow_at_top_nhds_iff {α : Type u_1} {n : } {c d : α} (hc : c 0) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top (nhds d) n = 0 c = d n < 0 d = 0
@[protected, instance]
theorem nhds_within_pos_comap_mul_left {α : Type u_1} {x : α} (hx : 0 < x) :
filter.comap (λ (ε : α), x * ε) (set.Ioi 0)) = (set.Ioi 0)
theorem eventually_nhds_within_pos_mul_left {α : Type u_1} {x : α} (hx : 0 < x) {p : α Prop} (h : ∀ᶠ (ε : α) in (set.Ioi 0), p ε) :
∀ᶠ (ε : α) in (set.Ioi 0), p (x * ε)