mdifferentiableWithinAt_univ — Mathlib

English

A function is differentiable within all space if and only if it is differentiable at that point.

Русский

Дифференцируемость внутри всего пространства эквивалентна обычной дифференцируемости в точке.

LaTeX

$$MDifferentiableWithinAt I I' f Set.univ x ↔ MDifferentiable I I' f x$$

Lean4

theorem mdifferentiableWithinAt_univ : MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x := by
  simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]

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