Theorem indicator_le_thickened_indicator_aux
Modification history
2022-06-06 14:27
src/topology/metric_space/thickened_indicator.lean
feat(measure_theory/measure/finite_measure_weak_convergence): Prove one implication of portmanteau theorem, convergence implies a limsup condition for measures of closed sets. (#14116) …
Added indicator_le_thickened_indicator_auxView on Github →