contDiffOn_restrContDiff_target — Mathlib

English

Let f be an OpenPartialHomeomorph between normed spaces E and F. For any n with n ≠ ∞, the inverse map f^{-1} is ContDiffOn of order n on the image of the restricted map, i.e., on the target of f.restrContDiff 𝕜 n hn.

Русский

Пусть f — частично открытая однородность между нормированными пространствами E и F. Для любого n с n ≠ ∞ обратная карта f^{-1} является ContDiffOn порядка n на изображении ограниченной карты, то есть на области определения f.restrContDiff 𝕜 n hn.

LaTeX

$$$$\operatorname{ContDiffOn}_{\mathbb{k}}(n, f^{-1}, \operatorname{target}(f\restriction_{\operatorname{ContDiff}_{\mathbb{k}}(n)}))$$$$

Lean4

theorem contDiffOn_restrContDiff_target (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
    ContDiffOn 𝕜 n f.symm (f.restrContDiff 𝕜 n hn).target := fun _x hx ↦ hx.2.1.contDiffWithinAt

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