English
Let V be a tangent-field-valued map on M. Then near x within s, V equals its pullback mpullbackWithin via extChartAt(x), in the sense of nhdsWithin equality.
Русский
Пусть V — отображение, принимающее значения в касательном пространстве, на M. Тогда в окрестности x внутри s значение V совпадает с его пуллбек-аналогом через extChartAt(x) в смысле эквивалентности по окружению nhdsWithin.
LaTeX
$$$\forall x \in s,\; (V =_ {\mathcal N[s]x} \mathrm{mpullbackWithin}_{\mathcal I}(\mathrm{extChartAt}\; I \; x) V).$$$
Lean4
theorem eventuallyEq_mpullback_mpullbackWithin_extChartAt (V : Π (x : M), TangentSpace I x) :
V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (extChartAt I x) (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I)) :=
by
apply nhdsWithin_le_nhds
filter_upwards [extChartAt_source_mem_nhds (I := I) x] with y hy
have A : (extChartAt I x).symm (extChartAt I x y) = y := (extChartAt I x).left_inv hy
rw [mpullback_apply, mpullbackWithin_apply, ← (isInvertible_mfderiv_extChartAt hy).inverse_comp_apply_of_right,
mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' hy, A]
simp only [ContinuousLinearMap.inverse_id, ContinuousLinearMap.coe_id', id_eq]
