Theorem MeasureTheory.tendstoInDistribution_of_ae_tendsto

Modification history

2026-05-29 07:38
Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
feat(MeasureTheory/Function): ae convergence implies convergence in distribution (#39517) …
Added MeasureTheory.tendstoInDistribution_of_ae_tendstoView on Github →