mathlib3
feat(topology): an `is_complete` set is a `complete_space`
#2037

Merged

feat(topology): an `is_complete` set is a `complete_space` #2037

mergify merged 6 commits into master from closeds-proof

feat(*): misc simple lemmas

de7d719a

+1 lemma

814b002a

Rename `inclusion_range` to `range_inclusion`

4dc553b4

feat(topology): an `is_complete` set is a `complete_space`

e4423e1a

Use in `finite_dimension`

b1921669

urkud added awaiting-review

Merge branch 'master' into closeds-proof

106fd2b0

sgouezel approved these changes on 2020-02-23

sgouezel removed awaiting-review

sgouezel added ready-to-merge

mergify merged 28e4bdfc into master 5 years ago

mergify deleted the closeds-proof branch 5 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone