Commit 2023-10-10 20:30 d34032a3

feat: compact subsets in products as cofiltered limits of projections (#6578) We exhibit a compact subset in a product of totally disconnected Hausdorff spaces as a limit of its projections to finite subsets of the indexing set, in the category Profinite. The proof is structured in the same way as Profinite.isIso_asLimitCone_lift and DiscreteQuotient.exists_of_compat.