inv — Mathlib

English

If f is a continuous map into a topological group, then the map x ↦ f(x)^{-1} is continuous.

Русский

Если f непрерывна в топологическую группу, то отображение x ↦ f(x)^{-1} непрерывно.

LaTeX

$$$\text{Continuous}(f) \Rightarrow \text{Continuous}(x \mapsto f(x)^{-1}).$$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem inv (hf : Continuous f) : Continuous fun x => (f x)⁻¹ :=
  continuous_inv.comp hf

Похожие утверждения