English
Let l be a filter on α and f: α → G₀ with limit a under l, where a ≠ 0. Then the inverse-valued function x ↦ (f(x))⁻¹ tends to a⁻¹ along l.
Русский
Пусть l — фильтр на α и функция f: α → G₀ имеет предел a по l, при этом a ≠ 0. Тогда функция x ↦ (f(x))⁻¹ стремится к a⁻¹ по l.
LaTeX
$$$\\operatorname{Tendsto} f\; l\\; (\\mathcal{N} a) \\land a \\neq 0 \\Rightarrow \\operatorname{Tendsto} (\\lambda x. f(x)^{-1})\\ l\\ (\\mathcal{N}(a^{-1})).$$$
Lean4
/-- If a function converges to a nonzero value, its inverse converges to the inverse of this value.
We use the name `Filter.Tendsto.inv₀` as `Filter.Tendsto.inv` is already used in multiplicative
topological groups. -/
theorem inv₀ {a : G₀} (hf : Tendsto f l (𝓝 a)) (ha : a ≠ 0) : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹) :=
(tendsto_inv₀ ha).comp hf
