congr — Mathlib

English

If a line-derivative statement holds for f, and f₁ agrees with f on the same set s, with the same value at x, then f₁ has the same line-derivative behavior on s.

Русский

Если для f выполняется утверждение о линейной производной, и f₁ совпадает с f на том же множестве s и в точке x, то у f₁ та же линейная производная на s.

LaTeX

$$$\text{HasLineDerivWithinAt}_{\mathbb{k}}(f,f',s,x,v) \Rightarrow \text{HasLineDerivWithinAt}_{\mathbb{k}}(f_1,f',s,x,v)$ при $f_1|_s = f|_s$ и $f_1(x)=f(x)$$$

Lean4

theorem congr (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : EqOn f₁ f s) (hx : f₁ x = f x) :
    HasLineDerivWithinAt 𝕜 f₁ f' s x v :=
  h.congr_mono hs hx (Subset.refl _)

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