isOpenMap_inclusion

Mathlib.Topology.Constructions

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

English

If S ⊆ T and S is open, then the inclusion map i: S → T is an open map.

Русский

Если S открыто в X и S ⊆ T, то включение S в T является открытым отображением.

LaTeX

$$$\text{IsOpenMap}(\text{inclusion } h)\,\text{ for } h:S\subseteq T,\; S\text{ open}. $$$

Lean4

theorem isOpenMap_inclusion {s t : Set X} (hs : IsOpen s) (h : s ⊆ t) : IsOpenMap (inclusion h) :=
  IsOpenMap.id.subtype_map hs h

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

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

Разделы

Аффилиация

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