codRestrict — Mathlib

English

If f is a closed 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 a closed map.

Русский

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

LaTeX

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

Lean4

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

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