congr — Mathlib

English

If f is differentiable within s and f1 equals f on s, then f1 is differentiable within s with the same derivative.

Русский

Если f дифференцируема внутри s и f1 совпадает с f на s, тогда f1 дифференцируема внутри s с той же производной.

LaTeX

$$$ \\mathrm{DifferentiableWithinAt}(f,s,x) \\to \\bigl(\\forall x\\in s, f_1(x)=f(x)\\bigr) \\to \\mathrm{DifferentiableWithinAt}(f_1,s,x) $$$

Lean4

theorem congr (h : DifferentiableWithinAt 𝕜 f s x) (ht : ∀ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) :
    DifferentiableWithinAt 𝕜 f₁ s x :=
  DifferentiableWithinAt.congr_mono h ht hx (Subset.refl _)

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