English
An analogue of HasFTaylorSeriesUpToOn for Pi with a prime construction: HasFTaylorSeriesUpToOn n Φ P' s is equivalent to the family-wise version with coordinate projections.
Русский
Аналог HasFTaylorSeriesUpToOn для Pi с проекциями координат: эквивалентность HasFTaylorSeriesUpToOn n Φ P' на s ко всем проекциям.
LaTeX
$$$ HasFTaylorSeriesUpToOn n \ Φ P' s \ \Longleftrightarrow\ \forall i, HasFTaylorSeriesUpToOn n (\\lambda x. Φ x i) (\\lambda x m. (ContinuousLinearMap.proj 𝕜 _ i).compContinuousMultilinearMap (P' x m)) s $$$
Lean4
@[simp]
theorem hasFTaylorSeriesUpToOn_pi' {n : WithTop ℕ∞} :
HasFTaylorSeriesUpToOn n Φ P' s ↔
∀ i,
HasFTaylorSeriesUpToOn n (fun x => Φ x i)
(fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap (P' x m)) s :=
by convert hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i); ext; rfl
