Theorems · Theorem · real analysis

HasFDerivWithinAt.abs

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {x : E}, HasFDerivWithinAt f f' s x → f x ≠ 0 → HasFDerivWithinAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') s x

Defined in

Mathlib.Analysis.Calculus.Deriv.Abs

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace