continuousOn — Mathlib

English

If a function f has a Taylor series up to order n on a set s, with a corresponding family p of formal multilinear series, then f is continuous on s.

Русский

Пусть функция f имеет разложение Тейлора до порядка n на множестве s, заданное семейством p формальных мультилинейных рядов; тогда f непрерывна на s.

LaTeX

$$$$\text{HasFTaylorSeriesUpToOn}(n,f,p,s) \Rightarrow \text{ContinuousOn}(f,s).$$$$

Lean4

theorem continuousOn (h : HasFTaylorSeriesUpToOn n f p s) : ContinuousOn f s :=
  by
  have := (h.cont 0 bot_le).congr fun x hx => (h.zero_eq' hx).symm
  rwa [← (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_continuousOn_iff]

Похожие утверждения