isBasis_basicOpen — Mathlib

English

The basis of opens given by basicOpen is a basis for the topology.

Русский

База открытых, заданная через basicOpen, является базисом топологии.

LaTeX

$$$$ \text{isBasis_basicOpen}(X) : \text{Opens.IsBasis}(\operatorname{Set.range}(X.basicOpen)). $$$$

Lean4

theorem isBasis_basicOpen (X : Scheme) [IsAffine X] : Opens.IsBasis (Set.range (X.basicOpen : Γ(X, ⊤) → X.Opens)) :=
  by
  convert
    PrimeSpectrum.isBasis_basic_opens.of_isInducing
      (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing using
    1
  ext V
  simp only [Set.mem_range, exists_exists_eq_and, Set.mem_setOf, ← Opens.coe_inj (V := V),
    ← Scheme.toSpecΓ_preimage_basicOpen]
  rfl

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