English
Let f: X → Y be a closed map. If S ⊆ X is closed, then the restriction f|_S: S → Y is a closed map. Equivalently, for every subset C ⊆ S that is closed in the subspace topology of S, the image f[C] is closed in Y.
Русский
Пусть f: X → Y замкнутое отображение. Если S ⊆ X замкнуто, то ограничение f|_S: S → Y является замкнутым отображением. То есть для любого множества C ⊆ S, замкнутого в подпространстве S, образ f[C] является замкнутым в Y.
LaTeX
$$$\\forall C \\subseteq S,\\; \\text{Closed}_S(C) \\Rightarrow f[C] \\text{ is closed in } Y,$ where $S$ is a closed subset of $X$ and $f|_S: S \\to Y$ is the restricted map.$$
Lean4
theorem restrict {f : X → Y} (hf : IsClosedMap f) {s : Set X} (hs : IsClosed s) : IsClosedMap (s.restrict f) :=
hf.comp hs.isClosedMap_subtype_val
