English
The affine opens form a topological basis for the opens of X.
Русский
Аффинные открытые образуют топологическую базису для открытых подмножеств X.
LaTeX
$$$$ \operatorname{Opens.IsBasis} \bigl(X.\text{affineOpens}\bigr). $$$$
Lean4
theorem isBasis_affine_open (X : Scheme) : Opens.IsBasis X.affineOpens :=
by
rw [Opens.isBasis_iff_nbhd]
rintro U x (hU : x ∈ (U : Set X))
obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen
refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩
rcases hS with ⟨i, rfl⟩
exact isAffineOpen_opensRange _