Commit 2026-05-27 10:16 baddb59a

View on Github →

chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap (#39762) Rename uniformContinuous_iff to uniformContinuous_iff_le_comap, to match continuous_iff_le_induced, and also to have symmetry with a possible lemma uniformContinuous_iff_map_le which doesn't exist now but could be added in the future.

Estimated changes

Modified Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

Modified Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

deleted theorem uniformContinuous_iff

added theorem uniformContinuous_iff_le_comap

Modified Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean