feat(topology/locally_constant): Adds a few useful constructions (#7954)
feat(topology/locally_constant): Adds a few useful constructions (#7954)

This PR adds a few useful constructions around locallly constant functions:
1. A locally constant function to `fin 2` associated to a clopen set.
2. Flipping a locally constant function taking values in a function type.
3. Unflipping a finite family of locally constant function.
4. Descending locally constant functions along an injective map.



Co-authored-by: Adam Topaz <d27a8cca44e6a02363c9f30139fa030f331183dc@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib