Zulip Chat Archive

Stream: new members

Topic: Heine-Cantor Theorem

Michael Lopez (Jun 16 2023 at 03:25):

Heine-Cantor Theorem.
I am trying to prove that a continuous function on a closed Ball (thus compact) is uniformly continuous. Does anybody know if this is in mathlib already?

Michael Lopez (Jun 16 2023 at 03:28):

I am trying to find the Heine-Cantor Theorem in mathlib. Does anybody know where to find it?

Notification Bot (Jun 16 2023 at 03:36):

Patrick Massot has marked this topic as unresolved.

Patrick Massot (Jun 16 2023 at 03:37):


Michael Lopez (Jun 16 2023 at 15:29):

Thank you!. I wonder now if there is a way to turn a Metric.closedBall type into a IsCompact type?

Patrick Massot (Jun 16 2023 at 16:12):

Do you mean docs4#ProperSpace.isCompact_closedBall ?

Jireh Loreaux (Jun 16 2023 at 16:32):

@Michael Lopez sometimes the best way is to ask on Zulip, but there's also a really handy tactic called exact? (this used to be called library_search) which can help you with this kind of thing. For example:

import Mathlib.Topology.Instances.Real

example (ε : ) (x : ) : IsCompact (Metric.closedBall x ε) := by
  exact? -- Try this: `exact isCompact_closedBall x ε`

Michael Lopez (Jun 16 2023 at 17:48):

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC