mdifferentiableOn_univ — Mathlib

English

If f is differentiable at x, then it is differentiable within any neighborhood of x.

Русский

Если функция дифференцируема в точке, то она дифференцируема внутри любой окрестности этой точки.

LaTeX

$$MDifferentiableAt I I' f x → MDifferentiableWithinAt I I' f s x$$

Lean4

theorem mdifferentiableOn_univ : MDifferentiableOn I I' f univ ↔ MDifferentiable I I' f := by
  simp only [MDifferentiableOn, mdifferentiableWithinAt_univ, mfld_simps]; rfl

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