hasGradientWithinAt_univ — Mathlib

English

HasGradientWithinAt f f' Set.univ x is equivalent to HasGradientAt f f' x.

Русский

Градиент внутри Set.univ совпадает с градиентом в точке x.

LaTeX

$$$\\text{HasGradientWithinAt } f f'\\ \\mathrm{Set.univ}\\ x \\iff \\text{HasGradientAt } f f'\\ x$$$

Lean4

@[simp]
theorem hasGradientWithinAt_univ : HasGradientWithinAt f f' univ x ↔ HasGradientAt f f' x :=
  by
  rw [hasGradientWithinAt_iff_hasFDerivWithinAt, hasGradientAt_iff_hasFDerivAt]
  exact hasFDerivWithinAt_univ

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