congr_mono — Mathlib

English

If h is a derivative within s and t ⊆ s, plus equality of function values on t, then HasDerivWithinAt on t holds.

Русский

Если h — производная внутри s, а t ⊆ s и значения функций совпадают на t, то отличие сохранится на t.

LaTeX

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

Lean4

theorem congr_mono (h : HasDerivWithinAt f f' s x) (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    HasDerivWithinAt f₁ f' t x :=
  HasFDerivWithinAt.congr_mono h ht hx h₁

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