Theorems · Theorem · real analysis
not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi
∀ (f : ℝ → ℝ) {a : ℝ},
Filter.Tendsto (deriv f) (nhdsWithin a (Set.Ioi a)) Filter.atBot → ¬DifferentiableWithinAt ℝ f (Set.Ioi a) aA real function whose derivative tends to minus infinity from the right at a point is not differentiable on the right at that point
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopproof · cited by 2,405
- nhdsWithinstatement and proof · cited by 1,912
- Set.Ioistatement and proof · cited by 1,463
- derivstatement and proof · cited by 676
- Filter.Tendsto.compproof · cited by 560
- Filter.atBotstatement and proof · cited by 512
- DifferentiableWithinAtstatement and proof · cited by 453
- Filter.tendsto_neg_atBot_atTopproof · cited by 22
- deriv.neg'proof · cited by 8
- DifferentiableWithinAt.negproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- Real.not_DifferentiableAt_log_mul_zeroproof · cited by 3
- InformationTheory.not_differentiableWithinAt_klFun_Ioi_zeroproof · cited by 1