locallyCompactSpace — Mathlib

English

The product of two locally compact spaces is locally compact.

Русский

Произведение двух локально компактных пространств локально компактно.

LaTeX

$$$\forall X\,Y\,[LocallyCompactSpace\;X]\,[LocallyCompactSpace\;Y] \Rightarrow LocallyCompactSpace\;(X\times Y)$$$

Lean4

instance locallyCompactSpace (X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X]
    [LocallyCompactSpace Y] : LocallyCompactSpace (X × Y) :=
  have := fun x : X × Y => (compact_basis_nhds x.1).prod_nhds' (compact_basis_nhds x.2)
  .of_hasBasis this fun _ _ ⟨⟨_, h₁⟩, _, h₂⟩ => h₁.prod h₂

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