borel_space): add `borelize` tactic (#12844)

Commit

3 years ago

feat(measure_theory/constructions/borel_space): add `borelize` tactic (#12844) Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

Author

urkud

Parents