English
Let s: B → E be a section; its differentiability at b0 is equivalent to the differentiability of the composed trivialization at b0.
Русский
Дифференцируемость секции s в точке b0 эквивалентна дифференцируемости композиции в тривиализации в b0.
LaTeX
$$$$MDifferentiableAt IB (IB.prod 𝓘(\mathbb{k}, F)) (\lambda b: \mathrm{TotalSpace.mk}' F b (s b)) b_0 \iff MDifferentiableAt IB 𝓘(\mathbb{k}, F) (\lambda b: (\text{trivializationAt } F E b_0 (s b)).2) b_0.$$$$
Lean4
/-- Characterization of differentiable sections of a vector bundle at a point within a set
in terms of the preferred trivialization at that point. -/
theorem mdifferentiableWithinAt_section (s : Π b, E b) {u : Set B} {b₀ : B} :
MDifferentiableWithinAt IB (IB.prod 𝓘(𝕜, F)) (fun b ↦ TotalSpace.mk' F b (s b)) u b₀ ↔
MDifferentiableWithinAt IB 𝓘(𝕜, F) (fun b ↦ (trivializationAt F E b₀ (s b)).2) u b₀ :=
by
rw [mdifferentiableWithinAt_totalSpace]
change MDifferentiableWithinAt _ _ id _ _ ∧ _ ↔ _
simp [mdifferentiableWithinAt_id]
