English
If f is a local diffeomorphism with inverse, and f is C^n at the inverse point with invertible differential, then the inverse is C^n at the corresponding point.
Русский
Если f является локальным гомеоморфизмом с обратной функцией, и если f в точке обратного образа является C^n с обратимой производной, то обратная функция — C^n в соответствующей точке.
LaTeX
$$$\\text{Let } f\\text{ be a local diffeomorphism with target containing } a.\\text{ If } f\\text{ is } C^n\\text{ at } f^{-1}(a)\\text{ and } Df_{f^{-1}(a)}\\text{ is a continuous linear isomorphism, then } f^{-1}\\text{ is } C^n \\text{ at } a.$$$
Lean4
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
@[fun_prop]
theorem prodMap' {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1) (hg : ContDiffAt 𝕜 n g p.2) :
ContDiffAt 𝕜 n (Prod.map f g) p :=
hf.prodMap hg
