completion): completion of metric spaces
#743

Merged

feat(topology/metric_space/completion): completion of metric spaces #743

digama0 merged 4 commits into leanprover-community:master from sgouezel:metric_completion

cipher1024 assigned

avigad 6 years ago

sgouezel force pushed from bac33385 to b8f9786c 6 years ago

completion of metric spaces

ebb635e2

name instance in metric_space.completion

d965e860

adapt to new filter member

77943b0e

rebase; adapt to new implicit arguments for uniformity

1f7f5197

sgouezel force pushed from b8f9786c to 1f7f5197 6 years ago

digama0 merged b9e9328e into master 6 years ago

sgouezel deleted the metric_completion branch 6 years ago

Reviewers

No reviews

Assignees

avigad

Labels

None yet

Milestone

No milestone