Commit 2022-08-27 13:27 c95908a6

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets. (#15321) Add equivalence of a limsup condition for closed sets and a liminf condition for open sets, which will later both be shown to be characterizing conditions of weak convergence of probability measures. Also add that either of these equivalent conditions implies that for any Borel set whose boundary carries zero probability in the candidate limit measure, we have that the measures of this set tend to its measure under the candidate limit measure.