congr — Mathlib

English

If h is MF-differentiable within at s and t ⊆ s with equality on t, then the mfderivWithin values are equal.

Русский

Если h дифференцируем внутри s, и t ⊆ s с равенством на t, то значения mfderivWithin равны.

LaTeX

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

Lean4

theorem congr (h : MDifferentiableWithinAt I I' f s x) (ht : ∀ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) :
    MDifferentiableWithinAt I I' f₁ s x :=
  (HasMFDerivWithinAt.congr_mono h.hasMFDerivWithinAt ht hx (Subset.refl _)).mdifferentiableWithinAt

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