gradient — Mathlib

English

If h : HasGradientWithinAt f f' s x and h₁ : (nhdsWithin x s).EventuallyEq f₁ f and hx : x ∈ s, then HasGradientWithinAt f₁ f' s x.

Русский

Если имеется градиент внутри s и f₁ эквивалентна f в окрестности x внутри s, и x ∈ s, тогда градиент сохраняется для f₁ внутри s.

LaTeX

$$HasGradientWithinAt f f' s x → (nhdsWithin x s).EventuallyEq f₁ f → Set.instMembership.mem s x → HasGradientWithinAt f₁ f' s x$$

Lean4

protected theorem gradient (h : f₁ =ᶠ[𝓝 x] f) : ∇ f₁ =ᶠ[𝓝 x] ∇ f :=
  h.eventuallyEq_nhds.mono fun _ h => h.gradient_eq

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