Theorem map_succ_at_top_eq

refactor(order/filter): generalize map_succ_at_top_eq to arbitrary Galois insertions; generalize tendsto_coe_iff to arbitary order-preserving embeddings

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): prove geometric series