feat(measure_theory): ext lemmas for measures (#3895)
Add class `sigma_finite`.
Also some cleanup.
Rename `measurable_space.is_measurable` -> `measurable_space.is_measurable'`. This is to avoid name clash with `_root_.is_measurable`, which should almost always be used instead.
define `is_pi_system`.
