isOpenEmbedding

Mathlib.Topology.Category.TopCat.OpenNhds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhds.isOpenEmbedding

English

For every x and open neighborhood U of x, the inclusion map from the underlying set U.1 into X is an open embedding.

Русский

Для каждого x и открытой окрестности U(x) включение из множества U.1 в X является открытым вложением.

LaTeX

$$IsOpenEmbedding U.1.inclusion'$$

Lean4

theorem isOpenEmbedding {x : X} (U : OpenNhds x) : IsOpenEmbedding U.1.inclusion' :=
  U.1.isOpenEmbedding

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

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

Разделы

Аффилиация

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