isAffine_affineBasisCover — Mathlib

English

Every member of an affine basis cover is affine.

Русский

Каждый элемент аффинной базы покрытия является аффинной схемой.

LaTeX

$$$$ \forall X:\text{AlgebraicGeometry.Scheme}, \forall i:\ X.\text{affineBasisCover}.I_0,\ \text{IsAffine}((X.\text{affineBasisCover}.X\ i)). $$$$

Lean4

instance isAffine_affineBasisCover (X : Scheme) (i : X.affineBasisCover.I₀) : IsAffine (X.affineBasisCover.X i) :=
  isAffine_Spec _

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