𝕜 : Type u_1
α : Type ?u.57235
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[Ioi 0] 0), p (x * ε)
𝕜 : Type u_1
α : Type ?u.57235
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p (x * ε)
rw [← nhdsWithin_pos_comap_mul_left hx]
no goals
𝕜 : Type u_1
α : Type ?u.57235
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[Ioi 0] 0), p (x * ε)
exact h.comap fun ε => x * ε