mdifferentiableOn — Mathlib

English

If f is differentiable on the whole domain with respect to I and I', then f is differentiable on any subset s with respect to I and I'.

Русский

Если функция f дифференцируема на всей области относительно структур I и I', то она дифференцируема на любом подмножестве s относительно тех же структур.

LaTeX

$$$MDifferentiable I I' f \\Rightarrow \\forall s\, MDifferentiableOn I I' f s$$$

Lean4

theorem mdifferentiableOn (h : MDifferentiable I I' f) : MDifferentiableOn I I' f s :=
  (mdifferentiableOn_univ.2 h).mono (subset_univ _)

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