locallyCompactSpace — Mathlib

English

If E is locally compact, then the model space H is locally compact as well.

Русский

Если E локально компактно, то и пространство H локально компактно.

LaTeX

$$LocallyCompactSpace H$$

Lean4

protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) : LocallyCompactSpace H :=
  by
  have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x) ∧ IsCompact s) fun s => I.symm '' (s ∩ range I) := fun x ↦
    by
    rw [← I.symm_map_nhdsWithin_range]
    exact ((compact_basis_nhds (I x)).inf_principal _).map _
  refine .of_hasBasis this ?_
  rintro x s ⟨-, hsc⟩
  exact (hsc.inter_right I.isClosed_range).image I.continuous_symm

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