Topologies on linear ordered fields

In this file we prove that a linear ordered field with order topology has continuous multiplication and division (apart from zero in the denominator). We also prove theorems like Filter.Tendsto.mul_atTop: if f tends to a positive number and g tends to positive infinity, then f * g tends to positive infinity.

theorem Filter.Tendsto.atTop_mul_pos {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atTop

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

@[deprecated Filter.Tendsto.atTop_mul_pos (since := "2025-03-18")]

theorem Filter.Tendsto.atTop_mul {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atTop

Alias of Filter.Tendsto.atTop_mul_pos.

---

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

theorem Filter.Tendsto.pos_mul_atTop {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x * g x) l atTop

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

@[deprecated Filter.Tendsto.pos_mul_atTop (since := "2025-03-18")]

theorem Filter.Tendsto.mul_atTop {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x * g x) l atTop

Alias of Filter.Tendsto.pos_mul_atTop.

---

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

@[simp]

theorem inv_atTop₀ {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.atTop⁻¹ = nhdsWithin 0 (Set.Ioi 0)

@[simp]

theorem inv_nhdsGT_zero {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : (nhdsWithin 0 (Set.Ioi 0))⁻¹ = Filter.atTop

theorem tendsto_inv_nhdsGT_zero {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

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

theorem tendsto_inv_atTop_nhdsGT_zero {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (r : 𝕜) => r⁻¹) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

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

theorem tendsto_inv_atTop_zero {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (r : 𝕜) => r⁻¹) Filter.atTop (nhds 0)

theorem Filter.Tendsto.inv_tendsto_atTop {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜} (h : Tendsto f l atTop) : Tendsto f⁻¹ l (nhds 0)

theorem Filter.Tendsto.inv_tendsto_nhdsGT_zero {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜} (h : Tendsto f l (nhdsWithin 0 (Set.Ioi 0))) : Tendsto f⁻¹ l atTop

theorem tendsto_pow_neg_atTop {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℕ} (hn : n ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => x ^ (-↑n)) Filter.atTop (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_atTop.

theorem tendsto_zpow_atTop_zero {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℤ} (hn : n < 0) : Filter.Tendsto (fun (x : 𝕜) => x ^ n) Filter.atTop (nhds 0)

@[instance 100]

instance IsStrictOrderedRing.toContinuousInv₀ {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] : ContinuousInv₀ 𝕜

@[deprecated IsStrictOrderedRing.toContinuousInv₀ (since := "2025-09-01")]

theorem IsStrictOrderedRing.toHasContinuousInv₀ {𝕜 : Type u_1} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] : ContinuousInv₀ 𝕜

Alias of IsStrictOrderedRing.toContinuousInv₀.

theorem IsTopologicalRing.of_norm {R : Type u_1} {𝕜 : Type u_2} [NonUnitalNonAssocRing R] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜) (norm_nonneg : ∀ (x : R), 0 ≤ norm x) (norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y) (nhds_basis : (nhds 0).HasBasis (fun (x : 𝕜) => 0 < x) fun (ε : 𝕜) => {x : R | norm x < ε}) : IsTopologicalRing R

If a (possibly non-unital and/or non-associative) ring R admits a submultiplicative nonnegative norm norm : R → 𝕜, where 𝕜 is a linear ordered field, and the open balls { x | norm x < ε }, ε > 0, form a basis of neighborhoods of zero, then R is a topological ring.

@[instance 100]

instance IsStrictOrderedRing.topologicalRing {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : IsTopologicalRing 𝕜

theorem Filter.Tendsto.atTop_mul_neg {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atBot

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

theorem Filter.Tendsto.neg_mul_atTop {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x * g x) l atBot

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

theorem Filter.Tendsto.atBot_mul_pos {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atBot

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

@[deprecated Filter.Tendsto.atBot_mul_pos (since := "2025-03-18")]

theorem Filter.Tendsto.atBot_mul {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atBot

Alias of Filter.Tendsto.atBot_mul_pos.

---

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

theorem Filter.Tendsto.atBot_mul_neg {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : α) => f x * g x) l atTop

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

theorem Filter.Tendsto.pos_mul_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x * g x) l atBot

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

@[deprecated Filter.Tendsto.pos_mul_atBot (since := "2025-03-18")]

theorem Filter.Tendsto.mul_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x * g x) l atBot

Alias of Filter.Tendsto.pos_mul_atBot.

---

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

theorem Filter.Tendsto.neg_mul_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x * g x) l atTop

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

@[simp]

theorem inv_atBot₀ {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.atBot⁻¹ = nhdsWithin 0 (Set.Iio 0)

@[simp]

theorem inv_nhdsLT_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : (nhdsWithin 0 (Set.Iio 0))⁻¹ = Filter.atBot

theorem tendsto_inv_nhdsLT_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => x⁻¹) (nhdsWithin 0 (Set.Iio 0)) Filter.atBot

The function x ↦ x⁻¹ tends to -∞ on the left of 0.

@[deprecated tendsto_inv_nhdsLT_zero (since := "2025-04-23")]

theorem tendsto_inv_zero_atBot {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => x⁻¹) (nhdsWithin 0 (Set.Iio 0)) Filter.atBot

Alias of tendsto_inv_nhdsLT_zero.

---

The function x ↦ x⁻¹ tends to -∞ on the left of 0.

theorem tendsto_inv_atBot_nhdsLT_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (r : 𝕜) => r⁻¹) Filter.atBot (nhdsWithin 0 (Set.Iio 0))

The function r ↦ r⁻¹ tends to 0 on the left as r → -∞.

@[deprecated tendsto_inv_atBot_nhdsLT_zero (since := "2025-04-23")]

theorem tendsto_inv_atBot_zero' {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (r : 𝕜) => r⁻¹) Filter.atBot (nhdsWithin 0 (Set.Iio 0))

Alias of tendsto_inv_atBot_nhdsLT_zero.

---

The function r ↦ r⁻¹ tends to 0 on the left as r → -∞.

theorem tendsto_inv_atBot_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : Filter.Tendsto (fun (r : 𝕜) => r⁻¹) Filter.atBot (nhds 0)

theorem Filter.Tendsto.div_atTop {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜} (h : Tendsto f l (nhds a)) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Filter.Tendsto.div_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜} (h : Tendsto f l (nhds a)) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Filter.Tendsto.const_div_atTop {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {g : α → 𝕜} (hg : Tendsto g l atTop) (r : 𝕜) : Tendsto (fun (n : α) => r / g n) l (nhds 0)

theorem Filter.Tendsto.const_div_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {g : α → 𝕜} (hg : Tendsto g l atBot) (r : 𝕜) : Tendsto (fun (n : α) => r / g n) l (nhds 0)

theorem Filter.Tendsto.inv_tendsto_atBot {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜} (h : Tendsto f l atBot) : Tendsto f⁻¹ l (nhds 0)

theorem Filter.Tendsto.inv_tendsto_nhdsLT_zero {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜} (h : Tendsto f l (nhdsWithin 0 (Set.Iio 0))) : Tendsto f⁻¹ l atBot

theorem bdd_le_mul_tendsto_zero' {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ (x : α) in l, |f x| ≤ C) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

If g tends to zero and there exists a constant C : 𝕜 such that eventually |f x| ≤ C, then the product f * g tends to zero.

theorem bdd_le_mul_tendsto_zero {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ (x : α) in l, b ≤ f x) (hB : ∀ᶠ (x : α) in l, f x ≤ B) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

If g tends to zero and there exist constants b B : 𝕜 such that eventually b ≤ f x| ≤ B, then the product f * g tends to zero.

theorem tendsto_bdd_div_atTop_nhds_zero {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ (x : α) in l, b ≤ f x) (hB : ∀ᶠ (x : α) in l, f x ≤ B) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

If g tends to atTop and there exist constants b B : 𝕜 such that eventually b ≤ f x| ≤ B, then the quotient f / g tends to zero.

theorem tendsto_const_mul_zpow_atTop_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℤ} {c : 𝕜} (hn : n < 0) : Filter.Tendsto (fun (x : 𝕜) => c * x ^ n) Filter.atTop (nhds 0)

theorem tendsto_const_mul_pow_nhds_iff' {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℕ} {c d : 𝕜} : Filter.Tendsto (fun (x : 𝕜) => c * x ^ n) Filter.atTop (nhds d) ↔ (c = 0 ∨ n = 0) ∧ c = d

theorem tendsto_const_mul_pow_nhds_iff {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => c * x ^ n) Filter.atTop (nhds d) ↔ n = 0 ∧ c = d

theorem tendsto_const_mul_zpow_atTop_nhds_iff {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => c * x ^ n) Filter.atTop (nhds d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

@[instance 100]

instance IsStrictOrderedRing.toIsTopologicalDivisionRing {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : IsTopologicalDivisionRing 𝕜

@[deprecated IsStrictOrderedRing.toIsTopologicalDivisionRing (since := "2025-03-25")]

theorem LinearOrderedField.toTopologicalDivisionRing {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : IsTopologicalDivisionRing 𝕜

Alias of IsStrictOrderedRing.toIsTopologicalDivisionRing.

theorem comap_mulLeft_nhdsGT_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : 𝕜} (hx : 0 < x) : Filter.comap (fun (x_1 : 𝕜) => x * x_1) (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 0 (Set.Ioi 0)

theorem eventually_nhdsGT_zero_mul_left {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop} (h : ∀ᶠ (ε : 𝕜) in nhdsWithin 0 (Set.Ioi 0), p ε) : ∀ᶠ (ε : 𝕜) in nhdsWithin 0 (Set.Ioi 0), p (x * ε)