differentiableWithinAt_univ — Mathlib

English

DifferentiableWithinAt 𝕜 f Set.univ x is equivalent to DifferentiableAt 𝕜 f x.

Русский

Дифференцируемость на всём множестве эквивалентна точечному дифференцируемому в x.

LaTeX

$$$$\\text{DifferentiableWithinAt } 𝕜 f\\,\\mathrm{Set.univ}\\,x \\iff \\text{DifferentiableAt } 𝕜 f\\,x.$$$$

Lean4

theorem differentiableWithinAt_univ : DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x := by
  simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]

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