Commit 2025-08-29 23:17 c9993f28

View on Github →

feat(Topology/UniformSpace/Ultra): completion is ultra uniformity iff base is (#27453) Supersedes #24628

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/NAry.lean

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.Eventually.eventually_prod_of_eventually_swap

added theorem Filter.Eventually.trans_prod

modified theorem Filter.prod_comm

Modified Mathlib/Topology/Constructions/SumProd.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean

added theorem IsSymmetricRel.image_prodMap

added theorem IsSymmetricRel.mem_filter_prod_comm

added theorem IsSymmetricRel.prod_subset_comm

Modified Mathlib/Topology/UniformSpace/Ultra/Basic.lean

added theorem IsTransitiveRel.mem_filter_prod_comm

added theorem IsTransitiveRel.mem_filter_prod_trans

added theorem IsTransitiveRel.prod_subset_trans

added theorem IsUltraUniformity.mem_nhds_iff_symm_trans

Created Mathlib/Topology/UniformSpace/Ultra/Completion.lean

added theorem IsSymmetricRel.cauchyFilter_gen

added theorem IsTransitiveRel.cauchyFilter_gen

added theorem IsUltraUniformity.cauchyFilter_iff

added theorem IsUltraUniformity.completion_iff

added theorem IsUltraUniformity.separationQuotient_iff

added theorem IsUniformInducing.isUltraUniformity