English
A function Φ: E → ∀ i, F'_i has ContDiffWithinAt n on s at x if and only if each coordinate Φ x i has ContDiffWithinAt n on s at x.
Русский
Функция Φ: E → ∀ i, F'_i имеет ContDiffWithinAt n на s в точке x тогда и только тогда каждая координата Φ x i имеет ContDiffWithinAt n на s в x.
LaTeX
$$$ ContDiffWithinAt 𝕜 n Φ s x \iff \forall i, ContDiffWithinAt 𝕜 n (\\lambda x. Φ x i) s x $$$
Lean4
theorem contDiffWithinAt_pi : ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x :=
by
set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
match n with
| ω =>
choose u hux p hp h'p using h
refine
⟨⋂ i, u i, Filter.iInter_mem.2 hux, _, hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _,
fun m ↦ ?_⟩
set L : (∀ i, E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] ∀ i, F' i := ContinuousMultilinearMap.piₗᵢ _ _
change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
| (n : ℕ∞) =>
intro m hm
choose u hux p hp using fun i => h i m hm
exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _, hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩
