mathlib

4d90ff97 - feat(topology/connected): Connectedness in sum and sigma type (#10511)

feat(topology/connected): Connectedness in sum and sigma type (#10511) This provides the `compact_space` and `totally_disconnected_space` instances for `α ⊕ β` and `Σ i, π i`.