English
In a fiber bundle, the preimage under the projection of a set with unique differentials in the base has unique differentials in the bundle, specialized to a point ⟨b, x⟩.
Русский
В расщеплении волокна предобраз по проекции множества имеет уникальные дифференциалы в расхождении над базой, конкретно для точки ⟨b, x⟩.
LaTeX
$$UniqueMDiffWithinAt.bundle_preimage' (hs) (x)$$
Lean4
/-- 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. -/
theorem uniqueDiffOn_inter_preimage (hs : UniqueMDiffOn I s) (x : M) (y : M'') {f : M → M''} (hf : ContinuousOn f s) :
UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) :=
haveI : UniqueMDiffOn I (s ∩ f ⁻¹' (extChartAt I' y).source) :=
by
intro z hz
apply (hs z hz.1).inter'
apply (hf z hz.1).preimage_mem_nhdsWithin
exact (isOpen_extChartAt_source y).mem_nhds hz.2
this.uniqueDiffOn_target_inter _
