Commit 2023-08-21 11:54 368923da
View on Github →feat: behavior of Cauchy
under operations on UniformSpace
(#6694)
Some of the lemmas are cherry-picked from leanprover-community/mathlib#17975 and will be useful for the general Arzela-Ascoli theorem, but I also filled some API holes on the way.