borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)

Commit

3 years ago

feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

Author

kex-y

Parents

86f80202

mathlib 70887f86 - feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)

mathlib
70887f86 - feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)