English
For glue data D and i, the composite of the i-th injection with the inverse of the glued Locally Ringed Space isomorphism equals the base immersion: (D_.ι i) ≫ (D.isoLocallyRingedSpace.inv) = (D.ι i).base.
Русский
Для данных склейки D и индекса i композиция между i-й инъекцией и обратной к сведению склейки из Locally Ringed Space совпадает с базовым внедрением: (D_.ι i) ≫ D.isoLocallyRingedSpace.inv = (D.ι i).base.
LaTeX
$$$(D_).\ι i \;≫\; D.isoLocallyRingedSpace.inv = (D.\ι i).base$$$
Lean4
instance (i j : 𝖣.J) : LocallyRingedSpace.IsOpenImmersion ((D.toLocallyRingedSpaceGlueData).toGlueData.f i j) := by
apply GlueData.f_open
