Mathlib Map

Theorems · Theorem · real analysis

HasFDerivWithinAt.arctan

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x
Defined in
Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Cited by
2 results in Mathlib
Foundations
Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroupNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DifferentiableWithinAt.arctan · cited by 1DifferentiableWithinAt.ar…fderivWithin_arctan · cited by 0fderivWithin_arctanSet · cited by 53352SetReal · cited by 25697RealRingHom.id · cited by 18349RingHom.idNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceContinuousLinearMap · cited by 5352ContinuousLinearMapStrongDual · cited by 459StrongDualHasFDerivWithinAt · cited by 356HasFDerivWithinAtReal.arctan · cited by 111Real.arctanHasDerivAt.comp_hasFDerivWithinAt · cited by 22HasDerivAt.comp_hasFDeriv…Real.hasDerivAt_arctan · cited by 7Real.hasDerivAt_arctanHasFDerivWithinAt.arctanCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.