Commit 2026-01-22 13:19 d45a6874

View on Github →

feat(Topology/Sets): define the Vietoris topology on (Nonempty)Compacts (#31059) This PR defines the Vietoris topology on Compacts and NonemptyCompacts, and proves that it is induced by the Hausdorff uniformity.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rel.lean

added theorem SetRel.preimage_eq_image

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Created Mathlib/Topology/Sets/VietorisTopology.lean

added theorem IsClosed.powerset_vietoris

added theorem IsOpen.powerset_vietoris

added theorem TopologicalSpace.Compacts.continuous_coe

added theorem TopologicalSpace.Compacts.isClopen_singleton_bot

added theorem TopologicalSpace.Compacts.isClosed_inter_nonempty_of_isClosed

added theorem TopologicalSpace.Compacts.isClosed_subsets_of_isClosed

added theorem TopologicalSpace.Compacts.isEmbedding_coe

added theorem TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen

added theorem TopologicalSpace.Compacts.isOpen_subsets_of_isOpen

added theorem TopologicalSpace.NonemptyCompacts.continuous_coe

added theorem TopologicalSpace.NonemptyCompacts.continuous_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isClosed_inter_nonempty_of_isClosed

added theorem TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed

added theorem TopologicalSpace.NonemptyCompacts.isEmbedding_coe

added theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen

added theorem TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen

added theorem TopologicalSpace.vietoris.isClopen_singleton_empty

added theorem TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed

added theorem TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen

Modified Mathlib/Topology/UniformSpace/Closeds.lean

added theorem IsCompact.nhds_hausdorff_eq_nhds_vietoris

deleted theorem TopologicalSpace.Compacts.isClosed_subsets_of_isClosed

deleted theorem TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen

deleted theorem TopologicalSpace.NonemptyCompacts.continuous_toCompacts

deleted theorem TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed

deleted theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts

deleted theorem TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen

added theorem TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage

added theorem TotallyBounded.nhds_vietoris_le_nhds_hausdorff

Modified docs/references.bib