Commit 2025-03-24 18:39 98c6231f

View on Github →

feat(Topology/UniformSpace/DiscreteUniformity): discrete uniformity (#23067)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

deleted theorem UniformSpace.DiscreteUnif.cauchy_le_pure

deleted theorem UniformSpace.DiscreteUnif.eq_const_of_cauchy

Created Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

added theorem DiscreteUniformity.eq_principal_idRel

added theorem DiscreteUniformity.eq_pure_cauchyConst

added theorem DiscreteUniformity.eq_pure_of_cauchy

added theorem DiscreteUniformity.idRel_mem_uniformity

added theorem DiscreteUniformity.uniformContinuous

added theorem discreteUniformity_iff_eq_principal_idRel

added theorem discreteUniformity_iff_idRel_mem_uniformity