# 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):

docs4#CompactSpace.uniformContinuous_of_continuous

#### 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