restrict — Mathlib

English

If f is an open map, s is open and ht is MapsTo f s t, then ht.restrict is open map.

Русский

Если f открытое отображение и s открыто, и ht = MapsTo f s t, то ht.restrict открытое отображение.

LaTeX

$$$\\forall f:X\\to Y,\\; \\text{IsOpenMap}(f) \\Rightarrow \\forall s,t,\\; \\text{IsOpen } s \\Rightarrow \\forall (ht:\\text{MapsTo } f s t), \\text{IsOpenMap}(ht.restrict).$$$

Lean4

theorem restrict {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {t : Set Y} (H : s.MapsTo f t) (hs : IsOpen s) :
    IsOpenEmbedding H.restrict :=
  ⟨hf.isEmbedding.restrict H,
    (by
      rw [MapsTo.range_restrict]
      exact continuous_subtype_val.1 _ (hf.isOpenMap _ hs))⟩

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