Commit 2025-12-21 15:46 6712d822

feat: Prokhorov theorem (#32701) We prove a version of Prokhorov theorem: given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set. We deduce that a tight set of probability measures has compact closure. We only assume that the space is T2 (no metrizability, no second-countability).