Commit 2019-12-23 23:32 64921a4c

refactor(topology/*): migrate to uniform_space.complete_of_convergent_controlled_sequences (#1821)

• refactor(topology/*): migrate to uniform_space.complete_of_convergent_controlled_sequences Also rewrite uniform_space.complete_of_convergent_controlled_sequences in terms of has_countable_basis, and add a lemma useful to prove l = ⨅ i, f i for filters.
• Revert some implicit/explicit argument changes No reason to have them, at least in this PR
• Fix docstrings
• Fix a docstring
• Fix imports
• cau_seq_filter: change namespaces, adjust hensel
• Fix compile
• Update src/topology/metric_space/cau_seq_filter.lean
• Update src/topology/uniform_space/cauchy.lean