antitone map. (#18001)

Commit

3 years ago

feat(analysis/bounded_variation): `evariation_on` of precomposition with monotone/antitone map. (#18001) Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>

Author

bottine

Parents

e9be2fa7

mathlib3 cd9a9326 - feat(analysis/bounded_variation): `evariation_on` of precomposition with monotone/antitone map. (#18001)

mathlib3
cd9a9326 - feat(analysis/bounded_variation): `evariation_on` of precomposition with monotone/antitone map. (#18001)