inv — Mathlib

English

If f is continuous within a set s at a point x, then the inverse function is continuous within s at x.

Русский

Если f непрерывна в пределах множества s в точке x, то функция-инверсия непрерывна в пределах s в x.

LaTeX

$$$\text{ContinuousWithinAt}(f,s,x) \Rightarrow \text{ContinuousWithinAt}(x \mapsto f(x)^{-1}, s, x).$$$

Lean4

@[to_additive]
nonrec theorem inv (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => (f x)⁻¹) s x :=
  hf.inv

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