lineDerivWithin_univ — Mathlib

English

The line derivative with respect to the ambient space equals the globally defined line derivative; restricting to the whole space does not change the derivative.

Русский

Производная вдоль линии по отношению к всей области совпадает с глобально определённой линейной производной; ограничение до всей области не изменяет её.

LaTeX

$$$\\mathrm{lineDerivWithin}_{\\mathbb{k}}(f, \\mathrm{univ}, x, v) = \\mathrm{lineDeriv}_{\\mathbb{k}}(f, x, v)$$$

Lean4

@[simp]
theorem lineDerivWithin_univ : lineDerivWithin 𝕜 f univ x v = lineDeriv 𝕜 f x v := by simp [lineDerivWithin, lineDeriv]

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