Theorem MeasureTheory.ProbabilityMeasure.tendsto_measure_of_isClopen_of_tendsto

Modification history

2025-08-03 17:11
Mathlib/MeasureTheory/Measure/Portmanteau.lean
feat: one implication of portmanteau theorem for countably generated filters (#27681) …
Added MeasureTheory.ProbabilityMeasure.tendsto_measure_of_isClopen_of_tendstoView on Github →