feat(topology/subset_properties): compact discrete spaces are finite (#6191) From lean-liquid
lean-liquid