weaklyLocallyCompactSpace — Mathlib

English

If X is weakly locally compact and s ⊆ X is closed, then the subspace s is weakly locally compact.

Русский

Если X имеет слабую локальную компактность, и s ⊆ X является замкнутым, то подпространство s обладает слабой локальной компактностью.

LaTeX

$$$\forall X\,[TopologicalSpace\;X]\,[WeaklyLocallyCompactSpace\;X]\ {s:Set\;X}, IsClosed\;s\rightarrow\WeaklyLocallyCompactSpace\;s$$$

Lean4

protected theorem weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace X] {s : Set X} (hs : IsClosed s) :
    WeaklyLocallyCompactSpace s :=
  hs.isClosedEmbedding_subtypeVal.weaklyLocallyCompactSpace

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