restrict — Mathlib

English

If f is an open map, then restricting f to an open set s gives an open map.

Русский

Если f — открытое отображение, ограничение на открытое множество s сохраняет открытость.

LaTeX

$$$$ \\text{IsOpenMap}(f) \\Rightarrow \\forall s\\ (\\text{IsOpen } s) \\Rightarrow \\text{IsOpenMap}(s.restrict f). $$$$

Lean4

theorem restrict {f : X → Y} (hf : IsOpenMap f) {s : Set X} (hs : IsOpen s) : IsOpenMap (s.restrict f) :=
  hf.comp hs.isOpenMap_subtype_val

Похожие утверждения