English
In a prespectral space, the opens determined by compact opens form a basis.
Русский
В prespectral-пространстве открытые множества, порожденные компактными открытыми, образуют базис.
LaTeX
$$$[\\mathrm{PrespectralSpace}(X)] \\Rightarrow \\mathrm{TopologicalSpace.Opens.IsBasis}(\\{U: \\ Opens X \\mid \\text{IsCompact}((U:\\ Set X))\\})$$$
Lean4
theorem isBasis_opens [PrespectralSpace X] : TopologicalSpace.Opens.IsBasis {U : Opens X | IsCompact (U : Set X)} :=
by
dsimp only [TopologicalSpace.Opens.IsBasis]
convert isTopologicalBasis (X := X)
ext s
exact ⟨fun ⟨V, hV, heq⟩ ↦ heq ▸ ⟨V.2, hV⟩, fun h ↦ ⟨⟨s, h.1⟩, h.2, rfl⟩⟩