## Stream: maths

### Topic: Heine–Borel

#### Johan Commelin (Feb 13 2020 at 06:26):

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

#### Yury G. Kudryashov (Feb 13 2020 at 06:30):

Yes, let me find a name.

#### Yury G. Kudryashov (Feb 13 2020 at 06:31):

compact_iff_closed_bounded

#### Johan Commelin (Feb 13 2020 at 06:31):

Aah, makes sense (-;

#### Johan Commelin (Feb 13 2020 at 06:31):

We should add Heine and Borel to the docstring

#### Johan Commelin (Feb 13 2020 at 06:31):

I'll do that in my PR

#### Kevin Buzzard (Feb 13 2020 at 07:47):

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

Last updated: May 19 2021 at 03:22 UTC