Commit 2022-03-21 07:40 8e9abe3c
View on Github →feat(measure_theory/constructions/borel_space): generalize a lemma (#12843)
Generalize measurable_limit_of_tendsto_metric_ae from
at_top : filter ℕ to any countably generated filter on a nonempty type.