Extension of function by continuity

Stream: Is there code for X?

[Igor Khavkine]

Is there any API in Mathlib about extending functions by continuity? Namely if $X, Y$ are topological spaces and $f\colon U \to Y$ is a continuous function on a dense subset $U \subset X$, then if there exists a continuous extension of $f$ to $\bar{f}\colon X \to Y$, then it is unique. Also if $f$ has appropriate continuity properties around the excluded points of $X \setminus U$, then the extension $\bar{f}$ can be defined by taking limits.

I've found something about extending continuous functions on a uniform space to its completion, but that's not immediately useful in this context.

[Rémy Degenne]

Dense.extend