cauchy): sequentially complete space with a countable basis is complete
#1761

Merged

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

mergify merged 5 commits into master from cauchy-filter-of-seq

sgouezel commented on 2019-12-01

feat(topology/uniform_space/cauchy): sequentially complete space with…

66dcabff

Add docs, drop unused section vars, make arguments `U` and `U'` expli…

54a6bbb4

urkud force pushed from 82a966b7 to 54a6bbb4 6 years ago

PatrickMassot commented on 2019-12-01

sgouezel commented on 2019-12-01

PatrickMassot commented on 2019-12-01

sgouezel commented on 2019-12-01

Update src/topology/uniform_space/cauchy.lean

7fbb7b47

Fix some comments

4ff0851c

Merge branch 'cauchy-filter-of-seq' of git://github.com/leanprover-co…

684fe8e8

sgouezel added ready-to-merge

sgouezel approved these changes on 2019-12-02

mergify merged 89fd0883 into master 6 years ago

mergify deleted the cauchy-filter-of-seq branch 6 years ago

Reviewers

sgouezel

bryangingechen

robertylewis

PatrickMassot

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone