mathlib

76f9c990 - feat(topology/subset_properties): add `sigma_compact_space` instances (#19100)

feat(topology/subset_properties): add `sigma_compact_space` instances (#19100) Add instances for * `α × β`, `α ⊕ β`, `ulift α`; * `Π i : ι, π i`, assuming `finite ι`; * `Σ i : ι, π i`, assuming `countable ι`. In each case, all input topological spaces are also assumed to be σ-compact. Motivated by the `prod` instance in the sphere eversion project.