Theorems · Theorem · real analysis

HasFDerivWithinAt.abs_of_neg

∀ {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|) (-f') s x

Defined in

Mathlib.Analysis.Calculus.Deriv.Abs

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace