mathlib3

2ed7e4ae - feat(analysis/bounded_variation): lower semicontinuity of `variation_on` (#18058)