Commit 2025-07-04 15:22 e47cd9bc

View on Github →

feat: monotonicity of lineMap (#26502) Also remove one assumption in differentiableOn_integral_of_continuous, and expand docstrings around this theorem.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

added theorem AffineMap.lineMap_anti

added theorem AffineMap.lineMap_mono

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean

modified theorem intervalIntegral.differentiableOn_integral_of_continuous

added theorem intervalIntegral.differentiable_integral_of_continuous

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

added theorem ContinuousAffineMap.coe_lineMap_eq