isBasis_affine_open — Mathlib

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 _

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