mono — Mathlib

English

If h : HasFTaylorSeriesUpToOn n f p s and hst : t ⊆ s, then HasFTaylorSeriesUpToOn n f p t.

Русский

Если h : HasFTaylorSeriesUpToOn n f p s и t ⊆ s, то HasFTaylorSeriesUpToOn n f p t.

LaTeX

$$HasFTaylorSeriesUpToOn\ n f p s → (t ⊆ s) → HasFTaylorSeriesUpToOn n f p t$$

Lean4

theorem mono (h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t ⊆ s) : HasFTaylorSeriesUpToOn n f p t :=
  ⟨fun x hx => h.zero_eq x (hst hx), fun m hm x hx => (h.fderivWithin m hm x (hst hx)).mono hst, fun m hm =>
    (h.cont m hm).mono hst⟩

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