Commit 2023-05-10 07:35 5d625662

View on Github →

feat: port Topology.Algebra.Equicontinuity (#3841)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Equicontinuity.lean

added theorem equicontinuous_of_equicontinuousAt_one

added theorem uniformEquicontinuous_of_equicontinuousAt_one