Commit 2023-03-05 22:29 002fae60

View on Github →

feat: port Topology.MetricSpace.Equicontinuity (#2638) Also changed a few small things in Topology/UniformSpace/Equicontinuity

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Equicontinuity.lean

added theorem Metric.equicontinuousAt_iff

added theorem Metric.equicontinuousAt_iff_right

added theorem Metric.equicontinuousAt_of_continuity_modulus

added theorem Metric.equicontinuous_of_continuity_modulus

added theorem Metric.uniformEquicontinuous_iff

added theorem Metric.uniformEquicontinuous_iff_right

added theorem Metric.uniformEquicontinuous_of_continuity_modulus

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean