English
If t is a neighborhood of x in the ambient space (not restricted to s), then HasMFDerivWithinAt I I' f (s ∩ t) x f' is equivalent to HasMFDerivWithinAt I I' f s x f'.
Русский
Если t является окрестностью x в окружающем пространстве, то HasMFDerivWithinAt I I' f (s ∩ t) x f' эквивалентно HasMFDerivWithinAt I I' f s x f'.
LaTeX
$$$ t \in \mathcal{N}(x) \;:\; HasMFDerivWithinAt I I' f (s \cap t) x f' \iff HasMFDerivWithinAt I I' f s x f' $$$
Lean4
theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f' :=
by
rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter,
continuousWithinAt_inter h]
exact extChartAt_preimage_mem_nhds h
