gradient_const' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem gradient_const' : ∇ (const F c) = 0 :=
  gradient_fun_const' c

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