Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-02 07:57 89fd0883

View on Github →

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

Estimated changes

Modified src/topology/uniform_space/cauchy.lean

added theorem cauchy_seq_of_controlled

added theorem le_nhds_of_cauchy_adhp_aux

added theorem sequentially_complete.le_nhds_of_seq_tendsto_nhds

added def sequentially_complete.seq

added theorem sequentially_complete.seq_is_cauchy_seq

added theorem sequentially_complete.seq_mem

added theorem sequentially_complete.seq_pair_mem

added def sequentially_complete.set_seq

added def sequentially_complete.set_seq_aux

added theorem sequentially_complete.set_seq_mem

added theorem sequentially_complete.set_seq_mono

added theorem sequentially_complete.set_seq_prod_subset

added theorem sequentially_complete.set_seq_sub_aux

added theorem uniform_space.complete_of_cauchy_seq_tendsto

added theorem uniform_space.complete_of_convergent_controlled_sequences