mathlib

a2d2e189 - feat(analysis/bounded_variation): some lemmas (#18108)

feat(analysis/bounded_variation): some lemmas (#18108) * The variation of a function on a set is zero iff the image of the set has zero diameter. * Two functions that are pointwise at distance zero on a set have equal variation on that set.