Theorem Union_neg

feat(topology): add Borel spaces

feat(data/set): add functions over sets

feat(topology/topological_space): add countablility and separability axioms for topological spaces

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

Merge branch 'master' of https://github.com/leanprover/mathlib

feat(topology/outer_measure): add outer measures and tools for Caratheodorys extension method