hasFDerivWithinAt_univ — Mathlib

English

For any f, f' and x, HasFDerivWithinAt on Set.univ x is equivalent to HasFDerivAt f f' x.

Русский

На всём пространстве эквивалентно HasFDerivWithinAt на Set.univ и HasFDerivAt в точке x.

LaTeX

$$$$\\text{HasFDerivWithinAt } f\\,f'\\,\\mathrm{Set.univ}\\,x \\iff \\text{HasFDerivAt } f\\,f'\\,x.$$$$

Lean4

@[simp]
theorem hasFDerivWithinAt_univ : HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f f' x := by
  simp only [HasFDerivWithinAt, nhdsWithin_univ, HasFDerivAt]

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