Commit 2023-12-04 06:38 2cf3f039

feat: uniqueness of weak limits of finite measures (#8498) This PR adds a type class HasOuterApproxClosed for topological spaces in which indicator functions of closed sets can be approximated from above by sequences of bounded continuous functions. All pseudo-(e)metrizable spaces satisfy this. In spaces with this property, finite Borel measures are characterized by the integrals of bounded continuous functions. Also weak limits of finite Borel measures are unique. More precisely, the topologies of weak convergence of finite Borel measures and of Borel probability measures are Hausdorff.