mfderivWithin_mono — Mathlib

English

If h is MDifferentiableWithinAt f s x and f1 ≈ f on nhdsWithin x (insert x s), then MDifferentiableWithinAt f1 s x.

Русский

Если h дифференцируемо внутри s в x и f1 приблизительно равен f в окрестности (insert x s), то f1 дифференцируемо внутри s в x.

LaTeX

$$$MDifferentiableWithinAt I I' f s x \Rightarrow (nhdsWithin x (\text{insert } x s)).EventuallyEq f_1 f) \Rightarrow MDifferentiableWithinAt I I' f_1 s x$$$

Lean4

theorem mfderivWithin_mono (h : MDifferentiableWithinAt I I' f s x) (hxt : UniqueMDiffWithinAt I t x) (h₁ : t ⊆ s) :
    mfderivWithin I I' f t x = mfderivWithin I I' f s x :=
  h.mfderivWithin_congr_mono (fun _ _ ↦ rfl) rfl hxt h₁

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