inv — Mathlib

English

If f is continuous on a set s, then the map x ↦ (f(x))^{-1} is continuous on s.

Русский

Если функция f непрерывна на подмножестве s, то отображение x ↦ (f(x))^{-1} непрерывно на s.

LaTeX

$$$\\mathrm{ContinuousOn}(f,s) \\Rightarrow \\mathrm{ContinuousOn}\\bigl(x \\mapsto (f(x))^{-1}, s\\bigr)$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem inv (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x)⁻¹) s := fun x hx ↦ (hf x hx).inv

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