instWeaklyLocallyCompactSpaceOfCompactSpace

English

A compact space is weakly locally compact; in fact, one may take the whole space as the required compact witness.

Русский

Компактное пространство является слабой локально компактной; допустимо взять всё пространство как требуемый компактный след.

LaTeX

$$$ \\text{Compact} \\Rightarrow \\text{WeaklyLocallyCompactSpace } X$$$

Lean4

instance (priority := 100) [CompactSpace X] : WeaklyLocallyCompactSpace X where
  exists_compact_mem_nhds _ := ⟨univ, isCompact_univ, univ_mem⟩

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