mdifferentiableWithinAt_congr — Mathlib

English

If h has MF-derivative within s at x and t ⊆ s, and f1 equals f on t and also at x, then f1 has MF-derivative within t at x with the same derivative.

Русский

Если h имеет MF-дериватив внутри s в x, и t ⊆ s, и f1 совпадает с f на t, а также в x, то f1 имеет MF-дериватив внутри t в x с тем же деривативом.

LaTeX

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

Lean4

theorem mdifferentiableWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
    MDifferentiableWithinAt I I' f₁ s x ↔ MDifferentiableWithinAt I I' f s x :=
  differentiableWithinAt_localInvariantProp.liftPropWithinAt_congr_iff h₁ hx

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