English
Let f: X → Y be a map between topological spaces and let s ⊆ Y. If x belongs to the preimage f^{-1}(s) and f is continuous at x, then the restriction of f to f^{-1}(s) viewed as a map f|_{f^{-1}(s)}: f^{-1}(s) → s is continuous at x.
Русский
Пусть f: X → Y — отображение между топологическими пространствами, пусть s ⊆ Y. Если x ∈ f^{-1}(s) и f непрерывна в точке x, то ограничение f на f^{-1}(s) как отображение f|_{f^{-1}(s)}: f^{-1}(s) → s непрерывно в x.
LaTeX
$$$\\forall f:X\\to Y,\\; \\forall s\\subseteq Y,\\; \\forall x\\in f^{-1}(s):\\; \\text{ContinuousAt}(f,x) \\Rightarrow \\text{ContinuousAt}\\left(f\\big|_{f^{-1}(s)}, x\\right).$$$
Lean4
theorem restrictPreimage {f : X → Y} {s : Set Y} {x : f ⁻¹' s} (h : ContinuousAt f x) :
ContinuousAt (s.restrictPreimage f) x :=
h.restrict _
