𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ Tendsto (fun x => x⁻¹) (𝓝[Ioi 0] 0) atTop
refine' (atTop_basis' 1).tendsto_right_iff.2 fun b hb => _
𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
hb' : 0 < b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
have hb' : 0 < b := by positivity
no goals
𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
hb' : 0 < b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
filter_upwards [Ioc_mem_nhdsWithin_Ioi
    ⟨le_rfl, inv_pos.2 hb'⟩]with x hx using(le_inv hx.1 hb').1 hx.2
no goals
𝕜 : Type u_1
α : Type ?u.24190
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
⊢ 0 < b
positivity