uniqueDiffOn_preimage — Mathlib

English

If h is a suitable n-diffeomorphism, then unique differentiability on a set is preserved through image by h.

Русский

Если h — подходящий n-диффеоморфизм, уникальная дифференцируемость множества сохраняется после образа через h.

LaTeX

$$UniqueDiffOn J (h '' s) ↔ UniqueDiffOn I s$$

Lean4

@[simp]
theorem uniqueDiffOn_preimage (h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F) (hn : 1 ≤ n) {s : Set F} :
    UniqueDiffOn 𝕜 (h ⁻¹' s) ↔ UniqueDiffOn 𝕜 s :=
  h.symm_image_eq_preimage s ▸ h.symm.uniqueDiffOn_image hn

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