emetric_space): redefine `diam`
#1941

Merged

refactor(topology/metric_space/emetric_space): redefine `diam` #1941

mergify merged 5 commits into master from ediam-redefine

feat(data/set/basic): define `set.subsingleton`

9c61c219

Add a missing lemma

b58b84ba

refactor(topology/metric_space/emetric_space): redefine `diam`

5569df6d

urkud added blocked-by-other-PR

cipher1024 assigned

sgouezel 6 years ago

urkud removed blocked-by-other-PR

Merge branch 'master' into ediam-redefine

4c7e5846

sgouezel commented on 2020-02-02

Redefine `set.subsingleton` using `(x ∈ s) (y ∈ s)`, prove `metric.di…

349586d8

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-02-03

mergify merged a3421322 into master 6 years ago

mergify deleted the ediam-redefine branch 6 years ago

Reviewers

sgouezel

Assignees

sgouezel

Labels

ready-to-merge

Milestone

No milestone