mathlib

mathlib copied to clipboard

Informally, this is the "minimum distance", though "minimum" makes sense mainly only in the finite context. This is analogous to diam in some sense. We provide finset and set versions for both the emetric and metric cases.

We generally try to have the analogous lemmas that diam has, and any other useful utility lemmas to allow for the use of the definition without unpacking it.

---

This commit does not represent finished work: I would like to open up a request for comment, and specifically would like some help filling out "blank lemmas": I'm happy to do the proving work, but as there's rather a lot of utility lemmas to fill out here, I want to make sure I'm doing so efficiently and not missing any. I also welcome general comment.

• [x] depends on: #16923
• [x] depends on: #16925

See discussion here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Opposite.20of.20diameter.20of.20an.20.28e.29metric.20space.2E

#12010 is relevant.

This PR/issue depends on:

• ~~leanprover-community/mathlib#16923~~
• ~~leanprover-community/mathlib#16925~~ By Dependent Issues (🤖). Happy coding!

LGTM, thanks! You can merge it once CI is happy. bors d+

:v: linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

LGTM, thanks! You can merge it once CI is happy. bors d+

Brilliant, thank you.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests