English
If a point x is within a set s and f is ContDiffWithinAt 𝕜′ n at x, then f is ContDiffWithinAt 𝕜 n at x after restricting scalars 𝕜.
Русский
Если точка x лежит внутри множества s и f имеет ContDiffWithinAt 𝕜′ n в точке x, то после ограничения скаляров 𝕜 получаем ContDiffWithinAt 𝕜 n в точке x.
LaTeX
$$$$\text{ContDiffWithinAt}_{𝕜' } n f s x \Rightarrow \text{ContDiffWithinAt}_{𝕜} n f s x.$$$$
Lean4
theorem restrict_scalars (h : ContDiffWithinAt 𝕜' n f s x) : ContDiffWithinAt 𝕜 n f s x := by
match n with
| ω =>
obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
exact ContinuousLinearMap.analyticOnNhd _ _
| (n : ℕ∞) =>
intro m hm
rcases h m hm with ⟨u, u_mem, p', hp'⟩
exact ⟨u, u_mem, _, hp'.restrictScalars _⟩
