weaklyLocallyCompactSpace — Mathlib

English

Let f: X → Y be a closed embedding. If Y is weakly locally compact, then X is weakly locally compact as well.

Русский

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

LaTeX

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

Lean4

protected theorem weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
    WeaklyLocallyCompactSpace X where
  exists_compact_mem_nhds
    x :=
    let ⟨K, hK, hKx⟩ := exists_compact_mem_nhds (f x)
    ⟨f ⁻¹' K, hf.isCompact_preimage hK, hf.continuous.continuousAt hKx⟩

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