isAffine_affineOpenCover — Mathlib

English

Each member of an affineOpenCover is affine.

Русский

Каждый элемент affineOpenCover является аффинной схемой.

LaTeX

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

Lean4

instance isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.I₀) : IsAffine (𝒰.openCover.X i) :=
  inferInstanceAs (IsAffine (Spec (𝒰.X i)))

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