mdifferentiableWithinAt_congr_of_mem

English

If h is MDifferentiableWithinAt f s x and f1 equals f on s, and x ∈ s, then f1 is MDifferentiableWithinAt f s x.

Русский

Если h имеет MDifferentiableWithinAt f s x и f1 совпадает с f на s, и x ∈ s, тогда f1 дифференцируема внутри s в x.

LaTeX

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

Lean4

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

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