locallyCompactSpace — Mathlib

English

If X is locally compact and f: X → Y is an open quotient map, then Y is locally compact.

Русский

Если X локально компактно и отображение f: X→Y является открытым факторизующим отображением, то Y локально компактно.

LaTeX

$$$[LocallyCompactSpace\;X] \{f:X\to Y\}, IsOpenQuotientMap\;f\rightarrow LocallyCompactSpace\;Y$$$

Lean4

theorem locallyCompactSpace [LocallyCompactSpace X] {f : X → Y} (hf : IsOpenQuotientMap f) : LocallyCompactSpace Y where
  local_compact_nhds := by
    refine hf.surjective.forall.2 fun x U hU ↦ ?_
    rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩
    exact ⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩

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