congr_mono — Mathlib

English

If a function f is differentiable on a set s, and f1 equals f on t ⊆ s, then f1 is differentiable on t.

Русский

Если функция f дифференцируема на множестве s, и f1 совпадает с f на t ⊆ s, то f1 дифференцируема на t.

LaTeX

$$$ \\mathrm{DifferentiableOn}(f,s) \\to \\mathrm{Set.EqOn}(f_1,f,t) \\to \\mathrm{DifferentiableOn}(f_1,t) $$$

Lean4

theorem congr_mono (h : DifferentiableOn 𝕜 f s) (h' : ∀ x ∈ t, f₁ x = f x) (h₁ : t ⊆ s) : DifferentiableOn 𝕜 f₁ t :=
  fun x hx => (h x (h₁ hx)).congr_mono h' (h' x hx) h₁

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