of_le — Mathlib

English

If HasFTaylorSeriesUpToOn n f p s and m ≤ n, then HasFTaylorSeriesUpToOn m f p s.

Русский

Если HasFTaylorSeriesUpToOn n f p s и m ≤ n, то HasFTaylorSeriesUpToOn m f p s.

LaTeX

$$HasFTaylorSeriesUpToOn\ n f p s → (m ≤ n) → HasFTaylorSeriesUpToOn m f p s$$

Lean4

theorem of_le (h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≤ n) : HasFTaylorSeriesUpToOn m f p s :=
  ⟨h.zero_eq, fun k hk x hx => h.fderivWithin k (lt_of_lt_of_le hk hmn) x hx, fun k hk => h.cont k (le_trans hk hmn)⟩

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