of_isTopologicalBasis — Mathlib

English

If a space X has a basis of opens consisting of compact sets, then X is prespectral.

Русский

Если пространство X имеет базис открытых множеств, состоящий из компактных множеств, то X является пресspectral.

LaTeX

$$$\\mathcal{B} \\text{ IsTopologicalBasis for } X \\,\\land\\; (\\forall U \\in \\mathcal{B}, \\ IsCompact(U)) \\Rightarrow \\mathrm{PrespectralSpace}(X)$$$

Lean4

/-- A space is prespectral if it has a basis consisting of compact opens. -/
theorem of_isTopologicalBasis {B : Set (Set X)} (basis : IsTopologicalBasis B)
    (isCompact_basis : ∀ U ∈ B, IsCompact U) : PrespectralSpace X where
  isTopologicalBasis := basis.of_isOpen_of_subset (fun _ h ↦ h.1) fun s hs ↦ ⟨basis.isOpen hs, isCompact_basis s hs⟩

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