feat(data/setoid/partition): indexed partition (#7910)
from LTE
Note that data/setoid/partition.lean, which already existed before this
PR, is currently not imported anywhere in mathlib. But it is used in LTE
and will be used in the next PR, in relation to locally constant
functions.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
