mathlib

ce23f373 - 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 <adamtopaz@users.noreply.github.com>