congr_mono — Mathlib

English

If ContDiffWithinAt holds for f on s, and f is equal to f1 on s1 ⊆ s with x mapped equally, then ContDiffWithinAt also holds for f1 on s1.

Русский

Если ContDiffWithinAt верно для f на s, и f совпадает с f1 на s1 ⊆ s, а x образуется одинаково, то ContDiffWithinAt верно и для f1 на s1.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow (s1 \\subseteq s) \\Rightarrow ContDiffWithinAt 𝕜 n f1 s1 x$$

Lean4

theorem congr_mono (h : ContDiffWithinAt 𝕜 n f s x) (h' : EqOn f₁ f s₁) (h₁ : s₁ ⊆ s) (hx : f₁ x = f x) :
    ContDiffWithinAt 𝕜 n f₁ s₁ x :=
  (h.mono h₁).congr h' hx

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