isClosedMap_subtype_val

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#IsClosed.isClosedMap_subtype_val

English

The map Subtype.val from a subtype into X is a closed map.

Русский

Отображение Subtype.val — замкнутое отображение.

LaTeX

$$$$ \\text{IsClosedMap}((\\uparrow):s\\to X). $$$$

Lean4

theorem isClosedMap_subtype_val {s : Set X} (hs : IsClosed s) : IsClosedMap ((↑) : s → X) :=
  hs.isClosedEmbedding_subtypeVal.isClosedMap

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru