Theorem TopologicalSpace.NonemptyCompacts.closure_finite_subsets

Modification history

2026-06-01 07:16
Mathlib/Topology/Sets/VietorisTopology.lean
feat(Topology/Sets): finite sets are dense in `(Nonempty)Compacts` (#34273)
Added TopologicalSpace.NonemptyCompacts.closure_finite_subsetsView on Github →