mathlib

8e9abe3c - feat(measure_theory/constructions/borel_space): generalize a lemma (#12843)

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.