[Merged by Bors] - feat: port Topology.Algebra.Order.Field

Mathlib.lean

@@ -1248,6 +1248,7 @@ import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Topology.Algebra.Order.ExtendFrom
 import Mathlib.Topology.Algebra.Order.ExtrClosure
+import Mathlib.Topology.Algebra.Order.Field
 import Mathlib.Topology.Algebra.Order.Filter
 import Mathlib.Topology.Algebra.Order.Floor
 import Mathlib.Topology.Algebra.Order.Group

Mathlib/Order/Filter/Pointwise.lean

@@ -825,7 +825,6 @@ Note that `Filter α` is not a `Distrib` because `f * g + f * h` has cross terms
 lacks.
 -/
 
-
 theorem mul_add_subset : f * (g + h) ≤ f * g + f * h :=
   map₂_distrib_le_left mul_add
 #align filter.mul_add_subset Filter.mul_add_subset
@@ -908,7 +907,7 @@ theorem map_inv' : f⁻¹.map m = (f.map m)⁻¹ :=
 #align filter.map_neg' Filter.map_neg'
 
 @[to_additive]
-theorem Tendsto.inv_inv : Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹ := fun hf =>
+protected theorem Tendsto.inv_inv : Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹ := fun hf =>
   (Filter.map_inv' m).trans_le <| Filter.inv_le_inv hf
 #align filter.tendsto.inv_inv Filter.Tendsto.inv_inv
 #align filter.tendsto.neg_neg Filter.Tendsto.neg_neg
@@ -920,8 +919,9 @@ protected theorem map_div : (f / g).map m = f.map m / g.map m :=
 #align filter.map_sub Filter.map_sub
 
 @[to_additive]
-theorem Tendsto.div_div : Tendsto m f₁ f₂ → Tendsto m g₁ g₂ → Tendsto m (f₁ / g₁) (f₂ / g₂) :=
-  fun hf hg => (Filter.map_div m).trans_le <| Filter.div_le_div hf hg
+protected theorem Tendsto.div_div (hf : Tendsto m f₁ f₂) (hg : Tendsto m g₁ g₂) :
+    Tendsto m (f₁ / g₁) (f₂ / g₂) :=
+  (Filter.map_div m).trans_le <| Filter.div_le_div hf hg
 #align filter.tendsto.div_div Filter.Tendsto.div_div
 #align filter.tendsto.sub_sub Filter.Tendsto.sub_sub
 

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -37,9 +37,7 @@ topological space, group, topological group
 -/
 
 
-open Classical Set Filter TopologicalSpace Function
-
-open Classical Topology Filter Pointwise
+open Classical Set Filter TopologicalSpace Function Topology Pointwise
 
 universe u v w x
 

Mathlib/Topology/Algebra/GroupWithZero.lean

@@ -255,29 +255,60 @@ protected def mulRight₀ (c : α) (hc : c ≠ 0) : α ≃ₜ α :=
 #align homeomorph.mul_right₀ Homeomorph.mulRight₀
 
 @[simp]
-theorem coe_mulLeft₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulLeft₀ c hc) = (· * ·) c :=
+theorem coe_mulLeft₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulLeft₀ c hc) = (c * ·) :=
   rfl
 #align homeomorph.coe_mul_left₀ Homeomorph.coe_mulLeft₀
 
 @[simp]
 theorem mulLeft₀_symm_apply (c : α) (hc : c ≠ 0) :
-    ((Homeomorph.mulLeft₀ c hc).symm : α → α) = (· * ·) c⁻¹ :=
+    ((Homeomorph.mulLeft₀ c hc).symm : α → α) = (c⁻¹ * ·) :=
   rfl
 #align homeomorph.mul_left₀_symm_apply Homeomorph.mulLeft₀_symm_apply
 
 @[simp]
-theorem coe_mulRight₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = fun x => x * c :=
+theorem coe_mulRight₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = (· * c) :=
   rfl
 #align homeomorph.coe_mul_right₀ Homeomorph.coe_mulRight₀
 
 @[simp]
 theorem mulRight₀_symm_apply (c : α) (hc : c ≠ 0) :
-    ((Homeomorph.mulRight₀ c hc).symm : α → α) = fun x => x * c⁻¹ :=
+    ((Homeomorph.mulRight₀ c hc).symm : α → α) = (· * c⁻¹) :=
   rfl
 #align homeomorph.mul_right₀_symm_apply Homeomorph.mulRight₀_symm_apply
 
 end Homeomorph
 
+section map_comap
+
+variable [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {a : G₀}
+
+theorem map_mul_left_nhds₀ (ha : a ≠ 0) (b : G₀) : map (a * ·) (𝓝 b) = 𝓝 (a * b) :=
+  (Homeomorph.mulLeft₀ a ha).map_nhds_eq b
+
+theorem map_mul_left_nhds_one₀ (ha : a ≠ 0) : map (a * ·) (𝓝 1) = 𝓝 (a) := by
+  rw [map_mul_left_nhds₀ ha, mul_one]
+
+theorem map_mul_right_nhds₀ (ha : a ≠ 0) (b : G₀) : map (· * a) (𝓝 b) = 𝓝 (b * a) :=
+  (Homeomorph.mulRight₀ a ha).map_nhds_eq b
+
+theorem map_mul_right_nhds_one₀ (ha : a ≠ 0) : map (· * a) (𝓝 1) = 𝓝 (a) := by
+  rw [map_mul_right_nhds₀ ha, one_mul]
+
+theorem nhds_translation_mul_inv₀ (ha : a ≠ 0) : comap (· * a⁻¹) (𝓝 1) = 𝓝 a :=
+  ((Homeomorph.mulRight₀ a ha).symm.comap_nhds_eq 1).trans <| by simp
+
+/-- If a group with zero has continuous multiplication and `fun x ↦ x⁻¹` is continuous at one,
+then it is continuous at any unit. -/
+theorem HasContinuousInv₀.of_nhds_one (h : Tendsto Inv.inv (𝓝 (1 : G₀)) (𝓝 1)) :
+    HasContinuousInv₀ G₀ where
+  continuousAt_inv₀ x hx := by
+    have hx' := inv_ne_zero hx
+    rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
+      tendsto_map'_iff, tendsto_comap_iff]
+    simpa only [(· ∘ ·), mul_inv_rev, mul_inv_cancel_right₀ hx']
+
+end map_comap
+
 section Zpow
 
 variable [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀]

Mathlib/Topology/Algebra/Order/Field.lean

@@ -0,0 +1,239 @@
+/-
+Copyright (c) 2022 Benjamin Davidson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
+
+! This file was ported from Lean 3 source module topology.algebra.order.field
+! leanprover-community/mathlib commit 9a59dcb7a2d06bf55da57b9030169219980660cd
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Tactic.Positivity
+import Mathlib.Topology.Algebra.Order.Group
+import Mathlib.Topology.Algebra.Field
+
+/-!
+# 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.
+-/
+
+
+open Set Filter TopologicalSpace Function Topology Classical
+open OrderDual (toDual ofDual)
+
+/-- 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. -/
+theorem TopologicalRing.of_norm {R 𝕜 : Type _} [NonUnitalNonAssocRing R] [LinearOrderedField 𝕜]
+    [TopologicalSpace R] [TopologicalAddGroup R] (norm : R → 𝕜)
+    (norm_nonneg : ∀ x, 0 ≤ norm x) (norm_mul_le : ∀ x y, norm (x * y) ≤ norm x * norm y)
+    (nhds_basis : (𝓝 (0 : R)).HasBasis ((0 : 𝕜) < ·) (fun ε ↦ { x | norm x < ε })) :
+    TopologicalRing R := by
+  have h0 : ∀ f : R → R, ∀ c ≥ (0 : 𝕜), (∀ x, norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
+  · refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
+    rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩
+    refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩
+    exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ
+  apply TopologicalRing.of_add_group_of_nhds_zero
+  case hmul =>
+    refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
+    refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
+    simp only [sub_zero] at *
+    calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
+    _ < ε := mul_lt_of_le_one_of_lt_of_nonneg hx.le hy (norm_nonneg _)
+  case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)
+  case hmul_right =>
+    exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x =>
+      (norm_mul_le x y).trans_eq (mul_comm _ _)
+
+variable {𝕜 α : Type _} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+  {l : Filter α} {f g : α → 𝕜}
+
+-- see Note [lower instance priority]
+instance (priority := 100) LinearOrderedField.topologicalRing : TopologicalRing 𝕜 :=
+  .of_norm abs abs_nonneg (fun _ _ ↦ (abs_mul _ _).le) <| by
+    simpa using nhds_basis_abs_sub_lt (0 : 𝕜)
+
+/-- In a linearly ordered field 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.atTop_mul {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop)
+    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
+  refine' tendsto_atTop_mono' _ _ (hf.atTop_mul_const (half_pos hC))
+  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0]
+    with x hg hf using mul_le_mul_of_nonneg_left hg.le hf
+#align filter.tendsto.at_top_mul Filter.Tendsto.atTop_mul
+
+/-- In a linearly ordered field 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`. -/
+theorem Filter.Tendsto.mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
+    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop := by
+  simpa only [mul_comm] using hg.atTop_mul hC hf
+#align filter.tendsto.mul_at_top Filter.Tendsto.mul_atTop
+
+/-- 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.atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop)
+    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by
+  have := hf.atTop_mul (neg_pos.2 hC) hg.neg
+  simpa only [(· ∘ ·), neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_atTop_atBot.comp this
+#align filter.tendsto.at_top_mul_neg Filter.Tendsto.atTop_mul_neg
+
+/-- 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.neg_mul_atTop {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
+    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot := by
+  simpa only [mul_comm] using hg.atTop_mul_neg hC hf
+#align filter.tendsto.neg_mul_at_top Filter.Tendsto.neg_mul_atTop
+
+/-- 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 {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot)
+    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by
+  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul hC hg
+  simpa [(· ∘ ·)] using tendsto_neg_atTop_atBot.comp this
+#align filter.tendsto.at_bot_mul Filter.Tendsto.atBot_mul
+
+/-- 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.atBot_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot)
+    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
+  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg
+  simpa [(· ∘ ·)] using tendsto_neg_atBot_atTop.comp this
+#align filter.tendsto.at_bot_mul_neg Filter.Tendsto.atBot_mul_neg
+
+/-- 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.mul_atBot {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
+    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot := by
+  simpa only [mul_comm] using hg.atBot_mul hC hf
+#align filter.tendsto.mul_at_bot Filter.Tendsto.mul_atBot
+
+/-- 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`. -/
+theorem Filter.Tendsto.neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
+    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop := by
+  simpa only [mul_comm] using hg.atBot_mul_neg hC hf
+#align filter.tendsto.neg_mul_at_bot Filter.Tendsto.neg_mul_atBot
+
+/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
+theorem tendsto_inv_zero_atTop : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop := by
+  refine' (atTop_basis' 1).tendsto_right_iff.2 fun b hb => _
+  have hb' : 0 < b := by positivity
+  filter_upwards [Ioc_mem_nhdsWithin_Ioi
+      ⟨le_rfl, inv_pos.2 hb'⟩]with x hx using(le_inv hx.1 hb').1 hx.2
+#align tendsto_inv_zero_at_top tendsto_inv_zero_atTop
+
+/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
+theorem tendsto_inv_atTop_zero' : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜)) := by
+  refine (atTop_basis.tendsto_iff ⟨fun s => mem_nhdsWithin_Ioi_iff_exists_Ioc_subset⟩).2 ?_
+  refine fun b hb => ⟨b⁻¹, trivial, fun x hx => ?_⟩
+  have : 0 < x := lt_of_lt_of_le (inv_pos.2 hb) hx
+  exact ⟨inv_pos.2 this, (inv_le this hb).2 hx⟩
+#align tendsto_inv_at_top_zero' tendsto_inv_atTop_zero'
+
+theorem tendsto_inv_atTop_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0) :=
+  tendsto_inv_atTop_zero'.mono_right inf_le_left
+#align tendsto_inv_at_top_zero tendsto_inv_atTop_zero
+
+theorem Filter.Tendsto.div_atTop {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) :
+    Tendsto (fun x => f x / g x) l (𝓝 0) := by
+  simp only [div_eq_mul_inv]
+  exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)
+#align filter.tendsto.div_at_top Filter.Tendsto.div_atTop
+
+theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0) :=
+  tendsto_inv_atTop_zero.comp h
+#align filter.tendsto.inv_tendsto_at_top Filter.Tendsto.inv_tendsto_atTop
+
+theorem Filter.Tendsto.inv_tendsto_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
+  tendsto_inv_zero_atTop.comp h
+#align filter.tendsto.inv_tendsto_zero Filter.Tendsto.inv_tendsto_zero
+
+/-- 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_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) :
+    Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by
+  simpa only [zpow_neg, zpow_ofNat] using (@tendsto_pow_atTop 𝕜 _ _ hn).inv_tendsto_atTop
+#align tendsto_pow_neg_at_top tendsto_pow_neg_atTop
+
+theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) :
+    Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0) := by
+  lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
+  rw [← neg_pos, ← h, Nat.cast_pos] at hn
+  simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'
+#align tendsto_zpow_at_top_zero tendsto_zpow_atTop_zero
+
+theorem tendsto_const_mul_zpow_atTop_zero {n : ℤ} {c : 𝕜} (hn : n < 0) :
+    Tendsto (fun x => c * x ^ n) atTop (𝓝 0) :=
+  mul_zero c ▸ Filter.Tendsto.const_mul c (tendsto_zpow_atTop_zero hn)
+#align tendsto_const_mul_zpow_at_top_zero tendsto_const_mul_zpow_atTop_zero
+
+theorem tendsto_const_mul_pow_nhds_iff' {n : ℕ} {c d : 𝕜} :
+    Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d := by
+  rcases eq_or_ne n 0 with (rfl | hn)
+  · simp [tendsto_const_nhds_iff]
+  rcases lt_trichotomy c 0 with (hc | rfl | hc)
+  · have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
+    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]
+  · simp [tendsto_const_nhds_iff]
+  · have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
+    simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]
+#align tendsto_const_mul_pow_nhds_iff' tendsto_const_mul_pow_nhds_iff'
+
+theorem tendsto_const_mul_pow_nhds_iff {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) :
+    Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d := by
+  simp [tendsto_const_mul_pow_nhds_iff', hc]
+#align tendsto_const_mul_pow_nhds_iff tendsto_const_mul_pow_nhds_iff
+
+theorem tendsto_const_mul_zpow_atTop_nhds_iff {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) :
+    Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0 := by
+  refine' ⟨fun h => _, fun h => _⟩
+  · cases n with -- porting note: Lean 3 proof used `by_cases`, then `lift` but `lift` failed
+    | ofNat n =>
+      left
+      simpa [tendsto_const_mul_pow_nhds_iff hc] using h
+    | negSucc n =>
+      have hn := Int.negSucc_lt_zero n
+      exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
+  · cases' h with h h
+    · simp only [h.left, h.right, zpow_zero, mul_one]
+      exact tendsto_const_nhds
+    · exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1
+#align tendsto_const_mul_zpow_at_top_nhds_iff tendsto_const_mul_zpow_atTop_nhds_iff
+
+-- see Note [lower instance priority]
+instance (priority := 100) LinearOrderedSemifield.toHasContinuousInv₀ {𝕜}
+    [LinearOrderedSemifield 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] :
+    HasContinuousInv₀ 𝕜 := .of_nhds_one <| tendsto_order.2 <| by
+  refine ⟨fun x hx => ?_, fun x hx => ?_⟩
+  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
+      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
+        max_lt hx one_half_lt_one⟩
+    filter_upwards [Ioo_mem_nhds one_pos (one_lt_inv h₀ h₁)] with y hy
+    exact hxx'.trans_lt <| inv_inv x' ▸ inv_lt_inv_of_lt hy.1 hy.2
+  · filter_upwards [Ioi_mem_nhds (inv_lt_one hx)] with y hy
+    simpa only [inv_inv] using inv_lt_inv_of_lt (inv_pos.2 <| one_pos.trans hx) hy
+
+instance (priority := 100) LinearOrderedField.toTopologicalDivisionRing :
+    TopologicalDivisionRing 𝕜 := ⟨⟩
+#align linear_ordered_field.to_topological_division_ring LinearOrderedField.toTopologicalDivisionRing
+
+-- porting note: todo: generalize to a `GroupWithzero`
+theorem nhdsWithin_pos_comap_mul_left {x : 𝕜} (hx : 0 < x) :
+    comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0 := by
+  rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]
+  congr 1
+  refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
+  simp
+#align nhds_within_pos_comap_mul_left nhdsWithin_pos_comap_mul_left
+
+theorem eventually_nhdsWithin_pos_mul_left {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop}
+    (h : ∀ᶠ ε in 𝓝[>] 0, p ε) : ∀ᶠ ε in 𝓝[>] 0, p (x * ε) := by
+  rw [← nhdsWithin_pos_comap_mul_left hx]
+  exact h.comap fun ε => x * ε
+#align eventually_nhds_within_pos_mul_left eventually_nhdsWithin_pos_mul_left

Mathlib/Topology/Homeomorph.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton
 
 ! This file was ported from Lean 3 source module topology.homeomorph
-! leanprover-community/mathlib commit d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
+! leanprover-community/mathlib commit 3b267e70a936eebb21ab546f49a8df34dd300b25
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -77,6 +77,9 @@ protected def symm (h : α ≃ₜ β) : β ≃ₜ α where
   toEquiv := h.toEquiv.symm
 #align homeomorph.symm Homeomorph.symm
 
+@[simp] theorem symm_symm (h : α ≃ₜ β) : h.symm.symm = h := rfl
+#align homeomorph.symm_symm Homeomorph.symm_symm
+
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
   because it is a composition of multiple projections. -/
 def Simps.apply (h : α ≃ₜ β) : α → β :=