Theorems · Theorem · real analysis
not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio
∀ (f : ℝ → ℝ) {a : ℝ},
Filter.Tendsto (deriv f) (nhdsWithin a (Set.Iio a)) Filter.atBot → ¬DifferentiableWithinAt ℝ f (Set.Iio a) aA real function whose derivative tends to minus infinity from the left at a point is not differentiable on the left 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.
Cites39
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
- mul_oneproof · cited by 3,885
- Filter.Tendstostatement and proof · cited by 3,814
- Nat.cast_oneproof · cited by 2,501
- nhdsWithinstatement and proof · cited by 1,912
- Filter.EventuallyEqproof · cited by 1,912
- Nat.cast_zeroproof · cited by 1,870
- Set.Ioiproof · cited by 1,463
- Set.Iooproof · cited by 1,214
- Set.Iiostatement and proof · cited by 1,166
- Set.Iicproof · cited by 1,111
- neg_negproof · cited by 960
Cited by2
Results whose statement or proof uses this declaration.
- InformationTheory.not_differentiableWithinAt_klFun_Iio_zeroproof · cited by 1
- not_differentiableWithinAt_of_deriv_tendsto_atTop_Iioproof · cited by 0