isProperMap_subtypeVal — Mathlib

English

The coercion from a closed subset is proper.

Русский

Выпуск принудительного отображения из замкнутого подмножества является правильным.

LaTeX

$$$IsProperMap((\uparrow): C \to X)$ for C closed subset$$

Lean4

/-- The coercion from a closed subset is proper. -/
theorem isProperMap_subtypeVal {C : Set X} (hC : IsClosed C) : IsProperMap ((↑) : C → X) :=
  hC.isClosedEmbedding_subtypeVal.isProperMap

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