instLocallyCompactPairOfLocallyCompactSpace

English

A reformulation: in a locally compact space, for a locally compact pair X,Y, there exists a neighborhood relation that maps compact sets to compact sets with a neighborhood relation preserved.

Русский

Переформулировка: в locally compact паре можно выбрать локальные компактные окрестности и отображения между ними сохраняют компактность.

LaTeX

$$$\forall X\,Y\,[TopologicalSpace\;X]\,[TopologicalSpace\;Y]\,[LocallyCompactSpace\;X]\,[LocallyCompactSpace\;Y]\ (\text{LocallyCompactPair } X\;Y)$$$

Lean4

instance (priority := 900) [LocallyCompactSpace X] : LocallyCompactPair X Y where
  exists_mem_nhds_isCompact_mapsTo hf
    hs :=
    let ⟨K, hKx, hKs, hKc⟩ := local_compact_nhds (hf.continuousAt hs);
    ⟨K, hKx, hKc, hKs⟩

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