mapsToRestrict — Mathlib

English

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

Русский

Если 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 mapsToRestrict {f : X → Y} (hf : IsOpenMap f) {s : Set X} {t : Set Y} (hs : IsOpen s) (ht : MapsTo f s t) :
    IsOpenMap ht.restrict :=
  (hf.restrict hs).codRestrict _

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