hasGradientWithinAt_congr_set — Mathlib

English

hasGradientWithinAt_congr_set: If nhds x eventually equals s and t, the HasGradientWithinAt statements are equivalent.

Русский

Если окрестности x эквиваленты множествам s и t, градиент внутри совпадает.

LaTeX

$$$\\text{HasGradientWithinAt } f f' s x \\bigl(\\text{nhds x} \\bigr) \\Rightarrow \\text{Iff}(\\text{HasGradientWithinAt } f f' s x, \\text{HasGradientWithinAt } f f' t x)$$$

Lean4

theorem hasGradientWithinAt_congr_set {s t : Set F} (h : s =ᶠ[𝓝 x] t) :
    HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x :=
  hasFDerivWithinAt_congr_set h

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