restrict — Mathlib

English

If f is an open embedding and H: s MapsTo f t with hs open, then H.restrict is an open embedding.

Русский

Если f — открытое вложение и H: s MapsTo f t, и s открыто, то H.restrict — открытое вложение.

LaTeX

$$$\\forall f:X\\to Y,\\; \\text{IsOpenEmbedding}(f) \\Rightarrow \\forall s,t,\\; (H:\\text{MapsTo } f s t), \\text{IsOpenEmbedding}(H).$$$

Lean4

theorem restrict {f : X → Y} (hf : IsEmbedding f) {s : Set X} {t : Set Y} (H : s.MapsTo f t) : IsEmbedding H.restrict :=
  .of_comp (hf.continuous.restrict H) continuous_subtype_val (hf.comp .subtypeVal)

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