isBasis_opens — Mathlib

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⟩⟩

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