English
The notion HasFTaylorSeriesUpToOn n f p univ is equivalent to HasFTaylorSeriesUpTo n f p on the whole space; formally, HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p.
Русский
Утверждение HasFTaylorSeriesUpToOn n f p univ эквивалентно HasFTaylorSeriesUpTo n f p; то есть локальное в унивальном случае равно глобальному.
LaTeX
$$$\text{HasFTaylorSeriesUpToOn } n f p \;\text{univ} \;\iff\; \text{HasFTaylorSeriesUpTo } n f p$$
Lean4
theorem hasFTaylorSeriesUpToOn_univ_iff : HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p :=
by
constructor
· intro H
constructor
· exact fun x => H.zero_eq x (mem_univ x)
· intro m hm x
rw [← hasFDerivWithinAt_univ]
exact H.fderivWithin m hm x (mem_univ x)
· intro m hm
rw [← continuousOn_univ]
exact H.cont m hm
· intro H
constructor
· exact fun x _ => H.zero_eq x
· intro m hm x _
rw [hasFDerivWithinAt_univ]
exact H.fderiv m hm x
· intro m hm
rw [continuousOn_univ]
exact H.cont m hm
