Zulip Chat Archive

Stream: maths

Topic: Heine–Borel


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 06:30):

Yes, let me find a name.

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 06:31):

compact_iff_closed_bounded

view this post on Zulip Johan Commelin (Feb 13 2020 at 06:31):

Aah, makes sense (-;

view this post on Zulip Johan Commelin (Feb 13 2020 at 06:31):

We should add Heine and Borel to the docstring

view this post on Zulip Johan Commelin (Feb 13 2020 at 06:31):

I'll do that in my PR

view this post on Zulip 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