English
A set-based version: if ψ, v, w are ContMDiffOn, then ψ(v, w) is ContMDiffOn on that set.
Русский
Версия на множестве: если ψ, v, w — ContMDiffOn, то ψ(v, w) дифференцируема на этом множестве.
LaTeX
$$$$\text{ContMDiffOn IM (IB. prod 𝓘(\mathbb{k}, F_1 \to_L F_2 \to_L F_3)) n (m \mapsto \mathrm{TotalSpace.mk}' F_3 (b(m)) (\psi(m)(v(m), w(m)))) s.$$$$
Lean4
/-- Characterization of differentiable functions into a vector bundle.
Version at a point within a set -/
theorem mdifferentiableWithinAt_totalSpace (f : M → TotalSpace F E) {s : Set M} {x₀ : M} :
MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F)) f s x₀ ↔
MDifferentiableWithinAt IM IB (fun x => (f x).proj) s x₀ ∧
MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (trivializationAt F E (f x₀).proj (f x)).2) s x₀ :=
by
simp +singlePass only [mdifferentiableWithinAt_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 (mdifferentiableWithinAt_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.mdifferentiableWithinAt_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]
