Heine-Cantor Theorem

Stream: new members

[Michael Lopez]

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]

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

[Notification Bot]

Patrick Massot has marked this topic as unresolved.

[Patrick Massot]

docs4#CompactSpace.uniformContinuous_of_continuous

[Michael Lopez]

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

[Patrick Massot]

Do you mean docs4#ProperSpace.isCompact_closedBall ?

[Jireh Loreaux]

@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]

Thank you!