𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝[Ioi 0] 0) = 𝓝[Ioi 0] 0
rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]
case e_a
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)
congr 1
case e_a
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.mulLeft₀ x (_ : x ≠ 0))) 0) = 𝓝 0
case e_a
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0
refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
no goals
case e_a
𝕜 : Type u_1
α : Type ?u.51715
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.mulLeft₀ x (_ : x ≠ 0))) 0) = 𝓝 0
simp