ι_isOpenEmbedding — Mathlib

English

For every index i, the map ι_i is an open embedding, i.e., it is an open map and an embedding.

Русский

Для каждого индекса i отображение ι_i является открывающим вложение: оно открыто и является вложением.

LaTeX

$$$\\iota_i \\colon 𝖣.U_i \\hookrightarrow \\text{glued}$ является открытым вложением.$$

Lean4

theorem ι_isOpenEmbedding (i : D.J) : IsOpenEmbedding (𝖣.ι i) :=
  .of_continuous_injective_isOpenMap (𝖣.ι i).hom.continuous_toFun (D.ι_injective i) fun U h =>
    D.open_image_open i ⟨U, h⟩

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