Theorems · Theorem · global analysis

UniqueMDiffOn.uniqueDiffOn_inter_preimage

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M'' : Type u_8} [inst_9 : TopologicalSpace M''] [inst_10 : ChartedSpace H' M''] {s : Set M} [IsManifold I 1 M],
  UniqueMDiff[s] →
    ∀ (x : M) (y : M'') {f : M → M''},
      ContinuousOn f s →
        UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

When considering functions between manifolds, this statement shows up often. It entails the unique differential of the pullback in extended charts of the set where the function can be read in the charts.

Defined in

Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Cited by

0 results in Mathlib

Foundations

Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifold