uniform convergence on a compact set

Stream: Is there code for X?

[Floris van Doorn]

Do we already have the following?
On a compact set, to show that a sequence of functions convergences uniformly (docs#tendsto_uniformly) it is sufficient to show that it converges pointwise.
The closest statement I can find is Heine-Cantor docs#is_compact.uniform_continuous_on_of_continuous
(@Patrick Massot)

[Sebastien Gouezel]

I am not sure I understand your statement. Consider the function f_n from [0, 1] to \R, which is equal to 0 at 0 and on [2/n, 1], to 1 at 1/n and affine inbetween. It converges pointwise to 0, but not uniformly.

[Floris van Doorn]

Ah, thanks for the counterexample. What I was thinking of was indeed false. I also think I figured out that in my actual application I can just use Heine-Cantor, so there's nothing to see here. Thanks for the answer!