congr' — Mathlib

English

If h holds for f on s, f₁ agrees with f on s, and x ∈ s, then the line-derivative statement remains valid for f₁ on s.

Русский

Если для f верно по отношению к s и f₁ совпадает с f на s, и x принадлежит s, то свойство линейной производной для f продолжает действовать для 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$ и $x\in s$$$

Lean4

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

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