Theorem nhds_principal_ne_top_of_is_lub

feat(topology): add Lebesgue measure

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