isOpenEmbedding — Mathlib

English

For any open subset U ⊆ X, the inclusion map i_U: U → X is an open embedding; it is a topological embedding with open image.

Русский

Для любого открытого подмножества U ⊆ X включение i_U: U → X является открытым вложением; это топологическое вложение с открытым образом.

LaTeX

$$$\\text{Inclusion}(U): U \\hookrightarrow X\\quad\\text{is an open embedding}$$$

Lean4

theorem isOpenEmbedding {X : TopCat.{u}} (U : Opens X) : IsOpenEmbedding (inclusion' U) :=
  U.2.isOpenEmbedding_subtypeVal

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