isOpenEmbedding_ι — Mathlib

English

The inclusion maps into the abstract finite coproduct in Sigma are open embeddings.

Русский

Включения в абстрактное конечное копроизведение в Σ являются открытыми вложениями.

LaTeX

$$$\\forall a:\\alpha,\\ IsOpenEmbedding(\\Sigma.\\ι X a)$$$

Lean4

/-- The inclusion maps into the abstract finite coproduct are open embeddings. -/
theorem isOpenEmbedding_ι (a : α) : IsOpenEmbedding (Sigma.ι X a) :=
  by
  refine
    IsOpenEmbedding.of_comp _
      (homeoOfIso ((colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))).isOpenEmbedding ?_
  convert finiteCoproduct.isOpenEmbedding_ι X a
  ext x
  change (Sigma.ι X a ≫ _) x = _
  simp

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