mapsToRestrict — Mathlib

English

If f is a closed map and s is closed, and ht is MapsTo f s t, then ht.restrict is a closed map.

Русский

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

LaTeX

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

Lean4

theorem mapsToRestrict {f : X → Y} (hf : IsClosedMap f) {s : Set X} {t : Set Y} (hs : IsClosed s) (ht : MapsTo f s t) :
    IsClosedMap ht.restrict :=
  (hf.restrict hs).codRestrict _

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