instWeaklyLocallyCompactSpaceOfLocallyCompactSpace

English

From LocallyCompactSpace X and Y, we obtain a LocallyCompactPair X Y.

Русский

Из локально компактного пространства X и Y следует локально компактная пара X Y.

LaTeX

$$$[LocallyCompactSpace\;X]\,[LocallyCompactSpace\;Y]\Rightarrow\text{LocallyCompactPair } X\;Y$$$

Lean4

instance (priority := 100) [LocallyCompactSpace X] : WeaklyLocallyCompactSpace X where
  exists_compact_mem_nhds
    (x : X) :=
    let ⟨K, hx, _, hKc⟩ := local_compact_nhds (x := x) univ_mem;
    ⟨K, hKc, hx⟩

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