norm_sq — Mathlib

English

If f and g are ContDiffWithinAt on s at x, then for all x ∈ s with f x ≠ g x, the function y ↦ ⟪f(y), g(y)⟫ is ContDiffWithinAt on s at x.

Русский

Если f и g дифференцируемы внутри s в x и f(x) ≠ g(x), то y ↦ ⟪f(y), g(y)⟫ дифференцируема внутри s в x.

LaTeX

$$$$\text{ContDiffWithinAt}_{\mathbb{R}}^n f\,s\,x \land \text{ContDiffWithinAt}_{\mathbb{R}}^n g\,s\,x \land f(x) \neq g(x) \Rightarrow \text{ContDiffWithinAt}_{\mathbb{R}}^n \big(y \mapsto \langle f(y), g(y)\rangle\big)\;s\;x.$$$$

Lean4

theorem norm_sq (hf : ContDiffOn ℝ n f s) : ContDiffOn ℝ n (fun y => ‖f y‖ ^ 2) s := fun x hx => (hf x hx).norm_sq 𝕜

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