English
If f converges to y in a multiplicative topological group, then f^{-1} converges to y^{-1}.
Русский
Если f стремится к y в мультипликативной топологической группе, то f^{-1} стремится к y^{-1}.
LaTeX
$$If $f: \alpha \to G$ and $\,\lim_{\alpha\to l} f = y$, then $\lim_{\alpha\to l} f^{-1} = y^{-1}$ in a topological group $G$.$$
Lean4
/-- If a function converges to a value in a multiplicative topological group, then its inverse
converges to the inverse of this value.
For the version in topological groups with zero (including topological fields)
assuming additionally that the limit is nonzero, use `Filter.Tendsto.inv₀`. -/
@[to_additive /-- If a function converges to a value in an additive topological group, then its
negation converges to the negation of this value. -/
]
theorem inv {f : α → G} {l : Filter α} {y : G} (h : Tendsto f l (𝓝 y)) : Tendsto (fun x => (f x)⁻¹) l (𝓝 y⁻¹) :=
(continuous_inv.tendsto y).comp h
