ι_isOpenEmbedding — Mathlib

English

For each open U, invApp f U is an iso.

Русский

Для каждого открытого U отображение invApp f U является изоморфизмом.

LaTeX

$$IsIso(H.invApp f U) for all U$$

Lean4

theorem ι_isOpenEmbedding [HasLimits C] (i : D.J) : IsOpenEmbedding (𝖣.ι i).base :=
  by
  rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _, TopCat.coe_comp]
  exact
    (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
      (D.toTopGlueData.ι_isOpenEmbedding i)

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