congr' — Mathlib

English

If f and f1 agree on s at x and the derivative exists, then HasFDerivWithinAt f1 f' s x holds.

Русский

Если f и f1 совпадают на s в точке x и существует производная, то HasFDerivWithinAt f1 f' s x выполняется.

LaTeX

$$$ \\mathrm{HasFDerivWithinAt}(f,f',s,x) \\to \\mathrm{Set.EqOn}(f_1,f,s) \\to \\mathrm{Eq}(f_1(x),f(x)) \\to \\mathrm{HasFDerivWithinAt}(f_1,f',s,x) $$$

Lean4

theorem congr' (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s) (hx : x ∈ s) : HasFDerivWithinAt f₁ f' s x :=
  h.congr hs (hs hx)

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