instIsOpenImmersionF — Mathlib

English

If two global sections over X restrict to equal sections on each member of an open cover, then they are equal globally.

Русский

Если две глобальные секции X ограничиваются равными секциями на каждом элементе открытого покрытия, то они равны глобально.

LaTeX

$$$$ \forall f,g,\; (\forall i, (\mathcal{U}.f i).app U f = (\mathcal{U}.f i).app U g) \Rightarrow f = g $$$$

Lean4

instance {X : Scheme.{u}} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : IsOpenImmersion (𝒰.f j) :=
  𝒰.map_prop j

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