subtype_map — Mathlib

English

If f: X → Y is a closed map and hs: IsClosed s, and hst: ∀x ∈ s, f(x) ∈ t, then the induced map on the subtype is closed.

Русский

Если f: X → Y замкнутое отображение и s замкнуто, а для x∈s верно f(x) ∈ t, то отображение между подтипами является замкнутым.

LaTeX

$$$\text{IsClosedMap}(f) \to (s \text{ closed}) \to (\forall x \in s, f(x) \in t) \Rightarrow \text{IsClosedMap}(\text{Subtype.map } f hst).$$$

Lean4

theorem subtype_map {f : X → Y} (hf : IsClosedMap f) {s : Set X} {t : Set Y} (hs : IsClosed s)
    (hst : ∀ x ∈ s, f x ∈ t) : IsClosedMap (Subtype.map f hst) :=
  (hf.comp hs.isClosedMap_subtype_val).subtype_mk _

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