mathlib
ef62d1c0 - chore(*): last preparations for Heine (#3179)

Commit
5 years ago
chore(*): last preparations for Heine (#3179) This is hopefully the last preparatory PR before we study compact uniform spaces. It has almost no mathematical content, except that I define `uniform_continuous_on`, and check it is equivalent to uniform continuity for the induced uniformity. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading