contDiffOn_inv — Mathlib

English

The inverse map Inv.inv is ContDiffOn 𝕜 n on the complement of {0}.

Русский

Обратная карта Inv.inv является ContDiffOn 𝕜 n на множествах, где аргумент не равен 0.

LaTeX

$$$\\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n (\\mathrm{Inv.inv}:\\mathbb{k'}\\to\\mathbb{k'})\\ {0}^{c}$$$

Lean4

@[fun_prop]
theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}ᶜ := fun _ hx =>
  (contDiffAt_inv 𝕜 hx).contDiffWithinAt

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