Theorems · Theorem · global analysis
taylor_isLittleO_univ
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ},
ContDiff ℝ (↑n) f → (fun x => f x - taylorWithinEval f n Set.univ x₀ x) =o[nhds x₀] fun x => (x - x₀) ^ n- Defined in
- Mathlib.Analysis.Calculus.Taylor
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- nhdsstatement · cited by 5,554
- ENatstatement · cited by 4,985
- Set.univstatement and proof · cited by 3,945
- WithTopstatement · cited by 3,754
- Set.mem_univproof · cited by 416
- Asymptotics.IsLittleOstatement and proof · cited by 375
- ContDiffstatement and proof · cited by 352
- nhdsWithin_univproof · cited by 88
- convex_univproof · cited by 53
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.taylor_charFun_twoproof · cited by 1