Heine–Borel

Stream: maths

[Johan Commelin]

Does mathlib know that a set in R^n is compact if and only if it is closed and bounded?

[Yury G. Kudryashov]

Yes, let me find a name.

[Yury G. Kudryashov]

compact_iff_closed_bounded

[Johan Commelin]

Aah, makes sense (-;

[Johan Commelin]

We should add Heine and Borel to the docstring

[Johan Commelin]

I'll do that in my PR

[Kevin Buzzard]

I've noticed time and time again that docstrings are a great place to store these "mathematician trigger" strings like Heine-Borel