mathlib

89fd0883 - feat(topology/uniform_space/cauchy): sequentially complete space with a countable basis is complete (#1761)

feat(topology/uniform_space/cauchy): sequentially complete space with a countable basis is complete (#1761) * feat(topology/uniform_space/cauchy): sequentially complete space with a countable basis is complete This is a more general version of what is currently proved in `cau_seq_filter`. Migration of the latter file to the new code will be done in a separate PR. * Add docs, drop unused section vars, make arguments `U` and `U'` explicit. * Update src/topology/uniform_space/cauchy.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Fix some comments