restrictPreimage_isClosedEmbedding

English

If f is a closed embedding, restricting its preimage remains a closed embedding.

Русский

Если f является замкнутым внедрением, ограничение предобраза сохраняет замкнутое внедрение.

LaTeX

$$$IsClosedEmbedding f \\rightarrow IsClosedEmbedding (s.restrictPreimage f)$$$

Lean4

theorem restrictPreimage_isClosedEmbedding (s : Set β) (h : IsClosedEmbedding f) :
    IsClosedEmbedding (s.restrictPreimage f) :=
  ⟨h.1.restrictPreimage s,
    (s.range_restrictPreimage f).symm ▸ IsInducing.subtypeVal.isClosed_preimage _ h.isClosed_range⟩

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