instWeaklyLocallyCompactSpaceForallOfFinite

English

Finite products of WeaklyLocallyCompactSpace spaces are WeaklyLocallyCompactSpace.

Русский

Конечные произведения пространств с слабой локальной компактностью сохраняют это свойство.

LaTeX

$$${\\iota}: \\text{Finite }\\iota \\Rightarrow \\text{WeaklyLocallyCompactSpace}(\\prod_{i\\in \\iota} X_i).$$$

Lean4

instance {ι : Type*} [Finite ι] {X : ι → Type*} [(i : ι) → TopologicalSpace (X i)]
    [(i : ι) → WeaklyLocallyCompactSpace (X i)] : WeaklyLocallyCompactSpace ((i : ι) → X i) where
  exists_compact_mem_nhds
    f := by
    choose s hsc hs using fun i ↦ exists_compact_mem_nhds (f i)
    exact ⟨pi univ s, isCompact_univ_pi hsc, set_pi_mem_nhds univ.toFinite fun i _ ↦ hs i⟩

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