congr_of_mem — Mathlib

English

If a function f has derivative f' within a set s at x, and another function f1 agrees with f on s, and x belongs to s, then f1 has derivative f' within s at x.

Русский

Пусть функция f имеет производную f′ внутри множества s в точке x, и другая функция f1 согласна с f на s, а x ∈ s. Тогда у f1 та же производная f′ внутри s в x.

LaTeX

$$$HasDerivWithinAt f f' s x \\rightarrow (\\forall y \\in s,\; f_1 y = f y) \\rightarrow x \\in s \\rightarrow HasDerivWithinAt f_1 f' s x$$$

Lean4

theorem congr_of_mem (h : HasDerivWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x) (hx : x ∈ s) :
    HasDerivWithinAt f₁ f' s x :=
  h.congr hs (hs _ hx)

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