mathlib

ffe70020 - feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant (#11708)

feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant (#11708) Gives an API for characteristic functions on clopen sets, `char_fn`, which are locally constant functions. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>