Theorems · Theorem · real analysis
HasDerivWithinAt.limsup_slope_le
∀ {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x r : ℝ},
HasDerivWithinAt f f' s x → f' < r → ∀ᶠ (z : ℝ) in nhdsWithin x (s \ {x}), slope f x z < r- Defined in
- Mathlib.Analysis.Calculus.Deriv.Slope
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Filter.Eventuallystatement · cited by 3,134
- nhdsWithinstatement · cited by 1,912
- Set.Iioproof · cited by 1,166
- IsOpen.mem_nhdsproof · cited by 470
- HasDerivWithinAtstatement and proof · cited by 333
- slopestatement · cited by 147
- isOpen_Iioproof · cited by 38
- hasDerivWithinAt_iff_tendsto_slopeproof · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.