mfderivWithin_congr_mono — Mathlib

English

If h is MDifferentiableWithinAt f s x and h₁: ∀y∈s, f1 y = f y, then MDifferentiableWithinAt f1 s x.

Русский

Если h имеет MDifferentiableWithinAt f s x и для всех y ∈ s выполняется f1 y = f y, то f1 имеет MDifferentiableWithinAt f s x.

LaTeX

$$$MDifferentiableWithinAt I I' f s x \Rightarrow (\forall y\in s, f_1 y = f y) \Rightarrow MDifferentiableWithinAt I I' f_1 s x$$$

Lean4

theorem mfderivWithin_congr_mono (h : MDifferentiableWithinAt I I' f s x) (hs : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x)
    (hxt : UniqueMDiffWithinAt I t x) (h₁ : t ⊆ s) : mfderivWithin I I' f₁ t x = mfderivWithin I I' f s x :=
  (HasMFDerivWithinAt.congr_mono h.hasMFDerivWithinAt hs hx h₁).mfderivWithin hxt

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