of_hasBasis — Mathlib

English

Locally compact spaces can be built from a basis of compact neighborhoods.

Русский

Локально-компактные пространства могут быть построены из базиса компактных окрестностей.

LaTeX

$$$\\forall X\\,[TopologicalSpace\\;X]\\,\\text{LocallyCompactSpace } X\\;\\Rightarrow\\; \\text{HasBasis-like construction}$$$

Lean4

theorem of_hasBasis {ι : X → Type*} {p : ∀ x, ι x → Prop} {s : ∀ x, ι x → Set X} (h : ∀ x, (𝓝 x).HasBasis (p x) (s x))
    (hc : ∀ x i, p x i → IsCompact (s x i)) : LocallyCompactSpace X :=
  ⟨fun x _t ht =>
    let ⟨i, hp, ht⟩ := (h x).mem_iff.1 ht
    ⟨s x i, (h x).mem_of_mem hp, ht, hc x i hp⟩⟩

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