mathlib3 documentation

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 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 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.

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

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

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 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 : α} :
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} [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) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top (nhds d) n = 0 c = d n < 0 d = 0
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 ε) :
∀ᶠ (ε : α) in nhds_within 0 (set.Ioi 0), p (x * ε)