mathlib

41e1ab75 - feat(topology/uniform_space/equicontinuity): definition and basic properties of [uniform] equicontinuity (#16467)