English
In a fiber bundle, the preimage under projection of a base set s with unique differentials also has unique differentials in the total space.
Русский
В волокне предобраз проекции базового множества s с уникальными дифференциалами также имеет уникальные дифференциалы в полном пространстве.
LaTeX
$$UniqueMDiffWithinAt.bundle_preimage$$
Lean4
/-- In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle. -/
theorem bundle_preimage {p : TotalSpace F Z} (hs : UniqueMDiffWithinAt I s p.proj) :
UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (π F Z ⁻¹' s) p :=
by
suffices UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (π F Z ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet)) p from
this.mono (by simp)
apply UniqueMDiffWithinAt.bundle_preimage_aux (hs.inter _) inter_subset_right
exact IsOpen.mem_nhds (trivializationAt F Z p.proj).open_baseSet (FiberBundle.mem_baseSet_trivializationAt' p.proj)
