ι_isOpenImmersion — Mathlib

English

In the LocallyRingedSpace gluing context, every point in the glued space arises from some chart after forgetting to the category of locally ringed spaces.

Русский

В контексте сшивки LocallyRingedSpace каждая точка слитого пространства восходит к точке из некоторой диаграммы после забывания до локально кольцевого пространства.

LaTeX

$$$\exists i, \exists y: D.U_i, (D.ι_i).base y = x$$$

Lean4

instance ι_isOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) :=
  by
  delta IsOpenImmersion; rw [← D.ι_isoSheafedSpace_inv]
  apply (config := { allowSynthFailures := true }) PresheafedSpace.IsOpenImmersion.comp
  exact (D.toSheafedSpaceGlueData).ιIsOpenImmersion i

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