chore(measure_theory): move, deduplicate (#9489)
* move lemmas like `is_compact.measure_lt_top` from `measure_theory.constructions.borel` to `measure_theory.measure.measure_space`;
* drop `is_compact.is_finite_measure` etc;
* add `measure_Ixx_lt_top`.
