of_isTopologicalBasis' — Mathlib

English

If {b_i} (i in I) forms a basis for X via the range of b, and each b_i is compact, then X is prespectral.

Русский

Если {b_i} (i в I) образуют базис пространства X через множество диапазона, и каждое b_i компактно, то X является prespectral.

LaTeX

$$$\\text{IsTopologicalBasis}(\\mathrm{SetRange}(b)) \\land (\\forall i, \\ IsCompact( b(i) )) \\Rightarrow \\mathrm{PrespectralSpace}(X)$$$

Lean4

/-- A space is prespectral if it has a basis consisting of compact opens.
This is the variant with an indexed basis instead. -/
theorem of_isTopologicalBasis' {ι : Type*} {b : ι → Set X} (basis : IsTopologicalBasis (Set.range b))
    (isCompact_basis : ∀ i, IsCompact (b i)) : PrespectralSpace X :=
  .of_isTopologicalBasis basis (by simp_all)

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