totalSpaceMk_isClosedEmbedding — Mathlib

English

If the base space B is T1, then the map TotalSpace.mk x is a closed embedding.

Русский

Если база является T1-пространством, то вложение TotalSpace.mk x является замкнутым вложением.

LaTeX

$$[T1Space B] (TotalSpace.mk x) isClosedEmbedding$$

Lean4

theorem totalSpaceMk_isClosedEmbedding [T1Space B] (x : B) : IsClosedEmbedding (@TotalSpace.mk B F E x) :=
  ⟨totalSpaceMk_isEmbedding F E x, by
    rw [TotalSpace.range_mk]
    exact isClosed_singleton.preimage <| continuous_proj F E⟩

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