isClosedMap_inclusion

Mathlib.Topology.Constructions

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

English

If S is closed and S ⊆ T, then the inclusion map i: S → T is a closed map.

Русский

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

LaTeX

$$$\text{IsClosedMap}(\text{inclusion } h)\;\text{ given }h:S\subseteq T\text{ and }S\text{ closed}. $$$

Lean4

theorem isClosedMap_inclusion {s t : Set X} (hs : IsClosed s) (h : s ⊆ t) : IsClosedMap (inclusion h) :=
  IsClosedMap.id.subtype_map hs h

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

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

Разделы

Аффилиация

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