Theorems · Theorem · global analysis

HasDerivWithinAt.norm_sq

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {f : ℝ → F} {f' : F} {s : Set ℝ}
  {x : ℝ}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 * inner ℝ (f x) f') s x

Defined in

Mathlib.Analysis.InnerProductSpace.Calculus

Cited by

0 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace