Commit 2025-11-30 04:06 ffc04d4a

View on Github →

feat(Analysis/Calculus/LHopital): L'Hopital's rule from within a convex set (#31408) Extracted from #19796

Estimated changes

Modified Mathlib/Analysis/Calculus/LHopital.lean

added theorem HasDerivWithinAt.lhopital_zero_nhdsWithin_convex

added theorem deriv.lhopital_zero_nhdsWithin_convex

added theorem derivWithin.lhopital_zero_nhdsWithin_convex

Modified Mathlib/Analysis/Convex/Topology.lean

added theorem Convex.Ioo_subset_of_mem_closure

added theorem Convex.diff_singleton_eventually_mem_nhds

added theorem Convex.nhdsWithin_diff_eq_nhdsGT

added theorem Convex.nhdsWithin_diff_eq_nhdsLT

added theorem Convex.nhdsWithin_diff_eq_nhdsNE

added theorem Convex.nhdsWithin_inter_Iio_eq_nhdsLT

added theorem Convex.nhdsWithin_inter_Ioi_eq_nhdsGT