mathlib3

473bb7d4 - feat(topology/locally_constant): basics on locally constant functions (#6192)

feat(topology/locally_constant): basics on locally constant functions (#6192) From `lean-liquid` Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>