gradient_eq

Mathlib.Analysis.Calculus.Gradient.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.gradient_eq

English

The gradient of a constant function is zero: ∇(const F c) x = 0 for all x.

Русский

Градиент константности равен нулю: ∇(константа c)(x) = 0 для всех x.

LaTeX

$$$\nabla(\text{const }F c)(x) = 0$$$

Lean4

theorem gradient_eq (hL : f₁ =ᶠ[𝓝 x] f) : ∇ f₁ x = ∇ f x :=
  by
  unfold gradient
  rwa [Filter.EventuallyEq.fderiv_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru