instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul

English

If α is T1, has continuous multiplication, and is WeaklyLocallyCompactSpace, then αˣ is WeaklyLocallyCompactSpace.

Русский

Если α T1, имеет непрерывное умножение и является слаб LocallyCompact, то αˣ — слаб LocallyCompact.

LaTeX

$$$ \\text{WeaklyLocallyCompactSpace}(\\alpha^{\\times}) $$$

Lean4

@[to_additive]
instance [T1Space α] [ContinuousMul α] [WeaklyLocallyCompactSpace α] : WeaklyLocallyCompactSpace αˣ :=
  isClosedEmbedding_embedProduct.weaklyLocallyCompactSpace

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