instLocallyCompactSpaceOfPrespectralSpace

English

If X is prespectral, then X is locally compact.

Русский

Если X prespectral, то X локально компактно.

LaTeX

$$$\\mathrm{PrespectralSpace}(X) \\Rightarrow \\mathrm{LocallyCompactSpace}(X)$$$

Lean4

instance (priority := low) [PrespectralSpace X] : LocallyCompactSpace X where
  local_compact_nhds _ _
    hn :=
    have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVn⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hn
    ⟨V, hV₁.mem_nhds hxV, hVn, hV₂⟩

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