congr — Mathlib

English

If h is a derivWithin within s and f1 equals f on s, then HasDerivWithinAt f1 f s x holds.

Русский

Если h — производная внутри s и f1 совпадает с f на s, тогда HasDerivWithinAt f1 f s x выполняется.

LaTeX

$$$$ HasDerivWithinAt f f' s x \\Rightarrow (∀ z ∈ s, f_1 z = f z) \\Rightarrow HasDerivWithinAt f_1 f' s x $$$$

Lean4

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

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