mathlib3

2d708803 - feat(topology/subset_properties): compact discrete spaces are finite (#6191)

feat(topology/subset_properties): compact discrete spaces are finite (#6191) From `lean-liquid` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Anne Baanen <vierkantor@vierkantor.com> Co-authored-by: Julian-Kuelshammer <julian.kuelshammer@math.uu.se> Co-authored-by: Jesse Michael Han <hyrodi@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Chase Meadors <c.ed.mead@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Calle Sönne <calle.sonne@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com> Co-authored-by: Adrián Doña Mateo <drnaia100@gmail.com>