weaklyLocallyCompactSpace — Mathlib

English

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

Русский

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

LaTeX

$$$\forall X\,Y\,[TopologicalSpace\;X]\,[TopologicalSpace\;Y]\,[WeaklyLocallyCompactSpace\;X]\ {f:X\to Y}, IsOpenQuotientMap\;f\rightarrow\WeaklyLocallyCompactSpace\;Y$$$

Lean4

theorem weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace X] {f : X → Y} (hf : IsOpenQuotientMap f) :
    WeaklyLocallyCompactSpace Y where
  exists_compact_mem_nhds := by
    refine hf.surjective.forall.2 fun x ↦ ?_
    rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩
    exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩

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