codRestrict — Mathlib

English

If f is an open map and every a maps into a fixed subset s (i.e., f(a) ∈ s for all a), then the codomain-restricted map s.codRestrict f hs is an open map.

Русский

Если f — открытое отображение и f(a) ∈ s для всех a, то отображение s.codRestrict f hs: X → s является открытым отображением.

LaTeX

$$$\\forall f:X\\to Y,\\; \\text{IsOpenMap}(f) \\Rightarrow \\forall s\\subseteq Y,\\; (\\forall a, f(a)\\in s) \\Rightarrow \\text{IsOpenMap}\\left(s\\codRestrict f hs\\right).$$$

Lean4

theorem codRestrict {f : X → Y} (hf : IsOpenMap f) {s : Set Y} (hs : ∀ a, f a ∈ s) : IsOpenMap (s.codRestrict f hs) :=
  hf.subtype_mk hs

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