instIsAffineXSchemeFiniteSubcover

English

A finite subcover of an affine open cover of a compact space remains affine.

Русский

Конечная подпокрывающая часть аффинного открытого покрытия компактного пространства остаётся аффинной.

LaTeX

$$$$ \forall X:\text{Scheme}, [\text{CompactSpace } X], (\mathcal{U}: X.\text{OpenCover}) [\forall i, \mathrm{IsAffine}(\mathcal{U}.X i)], i:\mathcal{U}.finiteSubcover.I_0 \Rightarrow \mathrm{IsAffine}(\mathcal{U}.finiteSubcover.X i). $$$$

Lean4

instance (X : Scheme) [CompactSpace X] (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.X i)] (i) :
    IsAffine (𝒰.finiteSubcover.X i) :=
  inferInstanceAs (IsAffine (𝒰.X _))

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