mathlib

6f75c57e - refactor(measure_theory/borel): `borel` is not an `instance` (#2326)

refactor(measure_theory/borel): `borel` is not an `instance` (#2326) Redo Borel spaces in a way similar to `closed_order_topology`/`order_topology`. * `borel` is no longer an `instance`; * define typeclass `opens_measurable_space` for a space with `measurable_space` and `topological_space` structures such that all open sets are measurable; * define typeclass `borel_space` for a space with `measurable_space` and `topological_space` structures such that `measurable_space` structure is equal to `borel`; * use dot syntax in more cases; * review some proofs that started to fail because of this change.