restrictPreimage — Mathlib

English

If f: X → Y is an embedding and s maps into t, then the restricted map H.restrict is an embedding.

Русский

Если f: X → Y — вложение (встраивание) и H: s → t является отображением, то H.restrict является вложением.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem restrictPreimage {f : X → Y} {s : Set Y} (h : Continuous f) : Continuous (s.restrictPreimage f) :=
  h.restrict _

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