isBasis_basicOpen — Mathlib

English

The range of basicOpen forms a basis for the topology on Proj 𝒜.

Русский

Образ функций basicOpen образует базис топологии на Proj 𝒜.

LaTeX

$$TopologicalBasis: IsBasis (Set.range (basicOpen 𝒜))$$

Lean4

theorem isBasis_basicOpen : TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜)) :=
  by
  delta TopologicalSpace.Opens.IsBasis
  convert ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜
  exact (Set.range_comp _ _).symm

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