isOpenMap_subtype_val

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#IsOpen.isOpenMap_subtype_val

English

If s is open, then the inclusion Subtype.val: s → X is an open embedding.

Русский

Если s открыто, то включение Subtype.val: s → X является открытым вложением.

LaTeX

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

Lean4

theorem isOpenMap_subtype_val {s : Set X} (hs : IsOpen s) : IsOpenMap ((↑) : s → X) :=
  hs.isOpenEmbedding_subtypeVal.isOpenMap

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

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

Разделы

Аффилиация

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