mathlib

b08c7ace - chore(topology/locally_finite): move from `topology.basic` (#15640)

chore(topology/locally_finite): move from `topology.basic` (#15640) Create a new file about `locally_finite`, move the definition and some lemmas from `topology.basic`.