Theorem MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'

Modification history

2025-10-28 16:45
Mathlib/MeasureTheory/Measure/Portmanteau.lean
feat: Lipschitz function criterion for weak convergence of probability measures (#30742) …
Added MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'View on Github →