mathlib

627bd0c2 - chore(topology/basic): use `finite` in `locally_finite_of_finite` (#15181)

chore(topology/basic): use `finite` in `locally_finite_of_finite` (#15181) Rename `locally_finite_of_fintype` to `locally_finite_of_finite`, use `[finite]` instead of `[fintype]`.