subtype_map — Mathlib

English

If f: X → Y is an open map and hp: ∀x, p(x) → p′(f(x)) holds (where p′ describes the target subtype), then the induced map on subtypes is open.

Русский

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

LaTeX

$$$\text{IsOpenMap}(f) \to (\forall x, p(x) \to p'(f(x))) \Rightarrow \text{IsOpenMap}(\text{Subtype.map } f hpq).$$$

Lean4

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

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