congr_mono — Mathlib

English

If h is MDifferentiableOn f s, and f1 equals f on t ⊆ s, then f1 is MDifferentiableOn f on t.

Русский

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

LaTeX

$$$MDifferentiableOn I I' f s \Rightarrow (\forall y\in t, f_1 y = f y) \Rightarrow t\subseteq s \Rightarrow MDifferentiableOn I I' f_1 t$$$

Lean4

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

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