Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC