norm_deriv_eq_norm_fderiv — Mathlib

English

For any differentiable f, the norm of the derivative at x equals the operator norm of the Frechet derivative: ‖deriv f x‖ = ‖fderiv 𝕜 f x‖.

Русский

Для любой дифференцируемой функции выполняется равенство норм производной в точке и операторной нормы Фрéш дифференциала: ‖deriv f x‖ = ‖fderiv 𝕜 f x‖.

LaTeX

$$$$ \\| \\operatorname{deriv} f x \\| = \\| fderiv 𝕜 f x \\| $$$$

Lean4

theorem norm_deriv_eq_norm_fderiv : ‖deriv f x‖ = ‖fderiv 𝕜 f x‖ := by simp [← deriv_fderiv]

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