Commit 2025-11-20 20:06 53cb4577

View on Github →

feat(Topology/UniformSpace): define the Hausdorff uniformity (#31031) This PR defines the Hausdorff uniformity on Closeds, Compacts and NonemptyCompacts. Since Closeds and NonemptyCompacts already have metrics, they are changed to use the newly defined uniformity.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rel.lean

added theorem SetRel.image_subset_image_left

added theorem SetRel.preimage_subset_preimage_left

added theorem SetRel.self_subset_image

added theorem SetRel.self_subset_preimage

Modified Mathlib/Topology/MetricSpace/Closeds.lean

deleted theorem EMetric.Closeds.isClosed_subsets_of_isClosed

deleted theorem EMetric.NonemptyCompacts.continuous_toCloseds

deleted theorem EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed

deleted theorem EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds

added theorem EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage

added theorem EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt

Modified Mathlib/Topology/Order.lean

added theorem isClosed_induced

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.Compacts.toCloseds_injective

added theorem TopologicalSpace.NonemptyCompacts.toCloseds_injective

added theorem TopologicalSpace.NonemptyCompacts.toCompacts_injective

Created Mathlib/Topology/UniformSpace/Closeds.lean

added theorem Filter.HasBasis.uniformity_closeds

added theorem Filter.HasBasis.uniformity_compacts

added theorem Filter.HasBasis.uniformity_hausdorff

added theorem Filter.HasBasis.uniformity_nonemptyCompacts

added theorem TopologicalSpace.Closeds.isClosed_subsets_of_isClosed

added theorem TopologicalSpace.Closeds.isOpen_inter_nonempty_of_isOpen

added theorem TopologicalSpace.Closeds.isUniformEmbedding_coe

added theorem TopologicalSpace.Closeds.uniformContinuous_coe

added theorem TopologicalSpace.Closeds.uniformity_def

added theorem TopologicalSpace.Compacts.continuous_toCloseds

added theorem TopologicalSpace.Compacts.isClosed_subsets_of_isClosed

added theorem TopologicalSpace.Compacts.isEmbedding_toCloseds

added theorem TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen

added theorem TopologicalSpace.Compacts.isUniformEmbedding_coe

added theorem TopologicalSpace.Compacts.isUniformEmbedding_toCloseds

added theorem TopologicalSpace.Compacts.uniformContinuous_coe

added theorem TopologicalSpace.Compacts.uniformContinuous_toCloseds

added theorem TopologicalSpace.Compacts.uniformity_def

added theorem TopologicalSpace.NonemptyCompacts.continuous_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.continuous_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed

added theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen

added theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe

added theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_coe

added theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.uniformity_def

added theorem UniformSpace.hausdorff.isClosed_powerset

added theorem UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen

added def hausdorffEntourage

added theorem hausdorffEntourage_comp

added theorem hausdorffEntourage_mono

added theorem inv_hausdorffEntourage

added theorem mem_hausdorffEntourage

added theorem monotone_hausdorffEntourage