preimage_openPartialHomeomorph — Mathlib

English

If a set s has UniqueMDiffOn and there is a appropriate preimage under charts, then unique MDiffOn holds for the preimage in tangent coordinates.

Русский

Если множество s имеет уникальное дифференциал, и существует подходящая предобразная карта, то для предобраза сохраняется уникальное MDiffOn в касательных координатах.

LaTeX

$$$UniqueMDiffOn\\ I\\ (s) \\Rightarrow UniqueMDiffOn\\ I\\text{ tangent preimage }$$$

Lean4

protected theorem preimage_openPartialHomeomorph (hs : UniqueMDiffWithinAt I s x) {e : OpenPartialHomeomorph M M'}
    (he : e.MDifferentiable I I') (hx : x ∈ e.source) : UniqueMDiffWithinAt I' (e.target ∩ e.symm ⁻¹' s) (e x) :=
  by
  rw [← e.image_source_inter_eq', inter_comm]
  exact
    (hs.inter (e.open_source.mem_nhds hx)).image_denseRange (he.mdifferentiableAt hx).hasMFDerivAt.hasMFDerivWithinAt
      (he.mfderiv_surjective hx).denseRange

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