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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto (function.uncurry has_mul.mul) ((nhds 0).prod (nhds x)) (nhds 0)
theorem
mul_tendsto_nhds_zero_left
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto (function.uncurry has_mul.mul) ((nhds x).prod (nhds 0)) (nhds 0)
theorem
nhds_eq_map_mul_left_nhds_one
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{x₀ : α}
(hx₀ : x₀ ≠ 0) :
nhds x₀ = filter.map (λ (x : α), x₀ * x) (nhds 1)
theorem
nhds_eq_map_mul_right_nhds_one
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{x₀ : α}
(hx₀ : x₀ ≠ 0) :
nhds x₀ = filter.map (λ (x : α), x * x₀) (nhds 1)
theorem
mul_tendsto_nhds_one_nhds_one
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
filter.tendsto (function.uncurry has_mul.mul) ((nhds 1).prod (nhds 1)) (nhds 1)
@[protected, instance]
def
linear_ordered_field.has_continuous_mul
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
theorem
filter.tendsto.at_top_mul
{α : Type u_1}
{β : Type u_2}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : 0 < C)
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l (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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : 0 < C)
(hf : filter.tendsto f l (nhds C))
(hg : filter.tendsto g l 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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : C < 0)
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l (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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : C < 0)
(hf : filter.tendsto f l (nhds C))
(hg : filter.tendsto g l 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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : 0 < C)
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l (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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : C < 0)
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l (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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : 0 < C)
(hf : filter.tendsto f l (nhds C))
(hg : filter.tendsto g l 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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α}
(hC : C < 0)
(hf : filter.tendsto f l (nhds C))
(hg : filter.tendsto g l 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}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
filter.tendsto (λ (x : α), x⁻¹) (nhds_within 0 (set.Ioi 0)) filter.at_top
The function x ↦ x⁻¹ tends to +∞ on the right of 0.
theorem
tendsto_inv_at_top_zero'
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
filter.tendsto (λ (r : α), r⁻¹) filter.at_top (nhds_within 0 (set.Ioi 0))
The function r ↦ r⁻¹ tends to 0 on the right as r → +∞.
theorem
tendsto_inv_at_top_zero
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
filter.tendsto (λ (r : α), r⁻¹) filter.at_top (nhds 0)
theorem
filter.tendsto.div_at_top
{α : Type u_1}
{β : Type u_2}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
[has_continuous_mul α]
{f g : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds a))
(hg : filter.tendsto g l 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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f : β → α}
(h : filter.tendsto f l filter.at_top) :
filter.tendsto f⁻¹ l (nhds 0)
theorem
filter.tendsto.inv_tendsto_zero
{α : Type u_1}
{β : Type u_2}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{l : filter β}
{f : β → α}
(h : filter.tendsto f l (nhds_within 0 (set.Ioi 0))) :
theorem
tendsto_pow_neg_at_top
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{n : ℕ}
{c d : α} :
theorem
tendsto_const_mul_pow_nhds_iff
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{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}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{n : ℤ}
{c d : α}
(hc : c ≠ 0) :
@[protected, instance]
def
linear_ordered_field.to_topological_division_ring
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α] :
theorem
nhds_within_pos_comap_mul_left
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{x : α}
(hx : 0 < x) :
filter.comap (λ (ε : α), x * ε) (nhds_within 0 (set.Ioi 0)) = nhds_within 0 (set.Ioi 0)
theorem
eventually_nhds_within_pos_mul_left
{α : Type u_1}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{x : α}
(hx : 0 < x)
{p : α → Prop}
(h : ∀ᶠ (ε : α) in nhds_within 0 (set.Ioi 0), p ε) :