Lipschitz functions on locally compact spaces

Stream: Is there code for X?

[Paul Lezeau]

Do we have the fact that if $X$ is a locally compact metric space and $f$ is locally Lipschitz on $X$ then it is Lipschitz on every compact subset of $X$?

[Anatole Dedecker]

I know @Benoît Guillemet is about to open a PR with this

[Anatole Dedecker]

The PR is #23349, it depends on #22890