range_glueDataObjι_ι_eq_support_inter

English

The range equality for the nested glue morphism equals the intersection of the scheme's support with the corresponding open, as previously stated.

Русский

Равенство диапазона вложенного глей-отображения равно пересечению опоры схемы и соответствующего открытого множества.

LaTeX

$$$ Set.range (I.glueDataObjι U ≫ U.1.ι).base = (I.support : Set X) \\cap U $$$

Lean4

theorem range_glueDataObjι_ι_eq_support_inter (U : X.affineOpens) :
    Set.range (I.glueDataObjι U ≫ U.1.ι).base = (I.support : Set X) ∩ U :=
  (I.range_glueDataObjι_ι U).trans (I.coe_support_inter U).symm

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