English
There is an order isomorphism between the lattice of opens of X and the lattice of ideals generated by compact opens of X in a prespectral space.
Русский
Существует лемма-изоморфизм между множеством открытых подмножеств X и множеством идеалов компактных открытых в prespectral пространстве.
LaTeX
$$$\\mathrm{Opens}(X) \\cong_o \\mathrm{Ideal}(\\mathrm{CompactOpens}(X))$$$
Lean4
instance sigma {ι : Type*} (X : ι → Type*) [∀ i, TopologicalSpace (X i)] [∀ i, PrespectralSpace (X i)] :
PrespectralSpace (Σ i, X i) :=
.of_isTopologicalBasis (IsTopologicalBasis.sigma fun i ↦ isTopologicalBasis) fun U hU ↦
by
simp_rw [Set.mem_iUnion] at hU
obtain ⟨i, V, hV, rfl⟩ := hU
exact hV.2.image continuous_sigmaMk
