Mathlib Map

Theorems · Theorem · real analysis

iteratedDerivWithin_eq_iteratedFDerivWithin

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
Defined in
Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Cited by
5 results in Mathlib
Foundations
Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNormedAddCommGroupNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

iteratedDerivWithin_succ · cited by 11iteratedDerivWithin_succiteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod · cited by 3iteratedFDerivWithin_appl…taylor_mean_remainder_lagrange_iteratedDeriv · cited by 1taylor_mean_remainder_lag…AbsolutelyMonotoneOn.iteratedDerivWithin_nonneg · cited by 1AbsolutelyMonotoneOn.iter…AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg · cited by 0AbsolutelyMonotoneOn.iff_…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceNontriviallyNormedField · cited by 8742NontriviallyNormedFieldContinuousMultilinearMap · cited by 1016ContinuousMultilinearMapiteratedFDerivWithin · cited by 147iteratedFDerivWithiniteratedDerivWithin · cited by 122iteratedDerivWithiniteratedDerivWithin_eq_iterat…CITED BYCITES

Cites8

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

Cited by5

Results whose statement or proof uses this declaration.