Commit 2026-06-01 07:16 0fea185d

View on Github →

feat(Topology/Sets): finite sets are dense in (Nonempty)Compacts (#34273)

Estimated changes

Modified Mathlib/Topology/Sets/VietorisTopology.lean

added theorem TopologicalSpace.Compacts.closure_finite_subsets

added theorem TopologicalSpace.Compacts.dense_setOf_finite

added theorem TopologicalSpace.NonemptyCompacts.closure_finite_subsets

added theorem TopologicalSpace.NonemptyCompacts.dense_setOf_finite

added theorem TopologicalSpace.vietoris.closure_finite_subsets