mathlib3

chore(topology): Splits topology.basic and topology.continuity

#785

Merged