mathlib3

1a7407d5 - feat(measure_theory/weak_convergence): define weak convergence of finite Borel measures