Theorem TopologicalSpace.NonemptyCompacts.dense_setOf_finite

Modification history

2026-07-17 09:57
Mathlib/Topology/Sets/VietorisTopology.lean
chore(Data): rename `setOf` to `Set.ofPred` (#41507) …
Deleted TopologicalSpace.NonemptyCompacts.dense_setOf_finiteView on Github →
2026-06-01 07:16
Mathlib/Topology/Sets/VietorisTopology.lean
feat(Topology/Sets): finite sets are dense in `(Nonempty)Compacts` (#34273)
Added TopologicalSpace.NonemptyCompacts.dense_setOf_finiteView on Github →