𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ ∀ (ib : 𝕜), ib ∈ Ioi 0 → ∃ ia, True ∧ ∀ (x : 𝕜), x ∈ Ici ia → x⁻¹ ∈ Ioc 0 ib
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ Tendsto (fun r => r⁻¹) atTop (𝓝[Ioi 0] 0)
refine (atTop_basis.tendsto_iff ⟨fun s => mem_nhdsWithin_Ioi_iff_exists_Ioc_subset⟩).2 ?_
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
⊢ x⁻¹ ∈ Ioc 0 b
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ ∀ (ib : 𝕜), ib ∈ Ioi 0 → ∃ ia, True ∧ ∀ (x : 𝕜), x ∈ Ici ia → x⁻¹ ∈ Ioc 0 ib
refine fun b hb => ⟨b⁻¹, trivial, fun x hx => ?_⟩
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
this : 0 < x
⊢ x⁻¹ ∈ Ioc 0 b
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
⊢ x⁻¹ ∈ Ioc 0 b
have : 0 < x := lt_of_lt_of_le (inv_pos.2 hb) hx
no goals
𝕜 : Type u_1
α : Type ?u.26472
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
this : 0 < x
⊢ x⁻¹ ∈ Ioc 0 b
exact ⟨inv_pos.2 this, (inv_le this hb).2 hx⟩