English
The total space of the bundle inherits a ContMDiff structure compatible with base and fiber charts, ensuring smoothness of bundle operations.
Русский
Общее пространство пучка наследует структуру ContMDiff, совместимую с базовой и волокновой чартами.
LaTeX
$$$$ ContMDiffTotalSpace(F,E) $$$$
Lean4
/-- Characterization of `C^n` functions into a vector bundle.
Version at a point within a set. -/
theorem contMDiffWithinAt_totalSpace {f : M → TotalSpace F E} {s : Set M} {x₀ : M} :
ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (trivializationAt F E (f x₀).proj (f x)).2) s x₀ :=
by
simp +singlePass only [contMDiffWithinAt_iff_target]
rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]
intro hf
simp_rw [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp_def, PartialEquiv.trans_apply,
PartialEquiv.prod_coe, PartialEquiv.refl_coe, extChartAt_self_apply, modelWithCornersSelf_coe, Function.id_def, ←
chartedSpaceSelf_prod]
refine (contMDiffWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)
have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
refine EventuallyEq.contMDiffWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
· simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]
rw [Trivialization.coe_fst']
exact hx
· simp only [mfld_simps]
