Commit 2023-06-07 12:30 3d3a4687

View on Github →

feat: port Analysis.Calculus.Monotone (#4792)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Monotone.lean

added theorem Monotone.ae_differentiableAt

added theorem Monotone.ae_hasDerivAt

added theorem MonotoneOn.ae_differentiableWithinAt

added theorem MonotoneOn.ae_differentiableWithinAt_of_mem

added theorem StieltjesFunction.ae_hasDerivAt

added theorem tendsto_apply_add_mul_sq_div_sub