uniqueMDiffOn_image — Mathlib

English

If h is a 1 ≤ n-class-diffeomorphism, then UniqueMDiffOn I on the preimage of a set equals UniqueMDiffOn J on the set.

Русский

Если h — диффеоморфизм с 1 ≤ n, то UniqueMDiffOn I на прообразе множества равен UniqueMDiffOn J на самом множестве.

LaTeX

$$UniqueMDiffOn I (h^{-1} s) ↔ UniqueMDiffOn J s$$

Lean4

@[simp]
theorem uniqueMDiffOn_image (h : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) {s : Set M} :
    UniqueMDiffOn J (h '' s) ↔ UniqueMDiffOn I s :=
  ⟨fun hs => h.symm_image_image s ▸ h.symm.uniqueMDiffOn_image_aux hn hs, h.uniqueMDiffOn_image_aux hn⟩

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