hasGradientWithinAt_congr_set' — Mathlib

English

HasGradientWithinAt_congr_set': if s and t are eventually equal, then HasGradientWithinAt f f' s x iff HasGradientWithinAt f f' t x.

Русский

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

LaTeX

$$$\\text{HasGradientWithinAt } f f' s x \\iff \\text{HasGradientWithinAt } f f' t x$ при $s =^{\\infty}_{\\ NHDS} t$$$

Lean4

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

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