mathlib

ce967b52 - feat(analysis/bounded_variation): remove [nonempty] from comp_anti/mono lemmas + golf (#18037)