Theorem tendsto_comp_succ_at_top_iff

refactor(order/filter): replace tendsto_comp_succ_at_top_iff by tendsto_add_at_top_iff_nat

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