norm_sq — Mathlib

English

Let f be differentiable over the real numbers. Then the map y ↦ ‖f(y)‖^2 is differentiable (as a real-valued function).

Русский

Пусть f: G → E дифференцируема по ℝ. Тогда отображение y ↦ ‖f(y)‖^2 дифференцируемо по ℝ (векторная функция замещается в скалярную).

LaTeX

$$$\forall f:\,G\to E,\;\text{Differentiable}_{\mathbb{R}}(f) \Rightarrow \text{Differentiable}_{\mathbb{R}}(y \mapsto \|f(y)\|^2)$.$$

Lean4

theorem norm_sq (hf : Differentiable ℝ f) : Differentiable ℝ fun y => ‖f y‖ ^ 2 := fun x => (hf x).norm_sq 𝕜

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