hasGradientWithinAt_const — Mathlib

English

If h : HasGradientWithinAt f f' s x, h₁ : f₁ =ᶠ[𝓝[s] x] f, hx : x ∈ s, then HasGradientWithinAt f₁ f' s x.

Русский

Если внутри s существует градиент и f₁ близка к f через nhdsWithin x s, и x ∈ s, то градиент сохраняется для f₁

LaTeX

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

Lean4

theorem hasGradientWithinAt_const : HasGradientWithinAt (fun _ => c) 0 s x :=
  hasGradientAtFilter_const _ _ _

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