instWeaklyLocallyCompactSpaceProd

English

The product of two WeaklyLocallyCompactSpace spaces is WeaklyLocallyCompactSpace.

Русский

Произведение двух слаб LocallyCompact-пространств является слаб LocallyCompact.

LaTeX

$$$[\\text{WeaklyLocallyCompactSpace } X]\\ [\\text{WeaklyLocallyCompactSpace } Y] \\Rightarrow \\text{WeaklyLocallyCompactSpace}(X \\times Y).$$$

Lean4

instance [WeaklyLocallyCompactSpace X] [WeaklyLocallyCompactSpace Y] : WeaklyLocallyCompactSpace (X × Y) where
  exists_compact_mem_nhds
    x :=
    let ⟨s₁, hc₁, h₁⟩ := exists_compact_mem_nhds x.1
    let ⟨s₂, hc₂, h₂⟩ := exists_compact_mem_nhds x.2
    ⟨s₁ ×ˢ s₂, hc₁.prod hc₂, prod_mem_nhds h₁ h₂⟩

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