English
If f is a function with MapsTo s t and is continuous at x, then its restriction to s is continuous at x.
Русский
Если f направлен в множество t из s и непрерывен в точке x, то ограничение функции на s непрерывно в x.
LaTeX
$$$\text{MapsTo}(f, s, t) \to \text{ContinuousAt}(f, x) \Rightarrow \text{ContinuousAt}(f|_s, x).$$$
Lean4
theorem restrict {f : X → Y} {s : Set X} {t : Set Y} (h1 : MapsTo f s t) {x : s} (h2 : ContinuousAt f x) :
ContinuousAt (h1.restrict f s t) x :=
(h2.comp continuousAt_subtype_val).codRestrict _