Theorem measure_theory.lebesgue_outer_is_measurable_Iio

feat(analysis/measure_theory): optimize proofs; trim, is_complete

feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable