locallyCompactSpace — Mathlib

English

The product of two locally compact spaces is locally compact.

Русский

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

LaTeX

$$$\forall (X:Y:):\; LocallyCompactSpace X\to LocallyCompactSpace Y\to LocallyCompactSpace (X\times Y)$$$

Lean4

protected theorem locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) :
    LocallyCompactSpace X :=
  hf.isInducing.locallyCompactSpace hf.isOpen_range.isLocallyClosed

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