ι_isoPresheafedSpace_inv — Mathlib

English

Each immersion ι_i is an open immersion after gluing, i.e., the glue data preserves open immersions componentwise.

Русский

Каждое вложение ι_i после сшивки является открытым вложением; сшивка сохраняет открытые вложения по компонентам.

LaTeX

$$$ι_i: U_i \hookrightarrow X$ isOpenImmersion$$

Lean4

theorem ι_isoPresheafedSpace_inv (i : D.J) :
    D.toPresheafedSpaceGlueData.toGlueData.ι i ≫ D.isoPresheafedSpace.inv = 𝖣.ι i :=
  𝖣.ι_gluedIso_inv _ _

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