English
For any filter f, a function m: α → ℝ≥0∞ and a ∈ ℝ≥0∞, Tendsto (m) to a is equivalent to Tendsto the inverse of m to a⁻¹. Precisely, Tendsto (x ↦ (m x)⁻¹) f (𝓝 a⁻¹) iff Tendsto m f (𝓝 a).
Русский
Для любого фильтра f, функции m: α → ℝ≥0∞ и точки a ∈ ℝ≥0∞ взаимно эквивалентны предельности: m сходится к a тогда и только тогда, когда обратная функция m сходится к a⁻¹.
LaTeX
$$$\\text{Tendsto}\\bigl( x \\mapsto (m(x))^{-1} \\bigr)\\ f\\ (\\mathcal{N} a^{-1}) \\iff \\text{Tendsto}\\ bigl( m \\bigr)\\ f\\ (\\mathcal{N} a).$$$
Lean4
@[simp] -- TODO: generalize to `[InvolutiveInv _] [ContinuousInv _]`
protected theorem tendsto_inv_iff {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹) ↔ Tendsto m f (𝓝 a) :=
⟨fun h => by simpa only [inv_inv] using Tendsto.inv h, Tendsto.inv⟩
