hasDerivWithinAt_univ — Mathlib

English

The derivative within the whole space univ is equivalent to the ordinary derivative at the point.

Русский

Производная внутри всего пространства равносильна обычной производной в точке.

LaTeX

$$$\text{HasDerivWithinAt } f f' \mathrm{univ} x \iff \text{HasDerivAt } f f' x$$$

Lean4

@[simp]
theorem hasDerivWithinAt_univ : HasDerivWithinAt f f' univ x ↔ HasDerivAt f f' x :=
  hasFDerivWithinAt_univ

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