local_compact_nhds — Mathlib

English

If X and Y are locally compact spaces, then their product X × Y is locally compact.

Русский

Произведение локально компактно, когда обе компоненты локально компактны.

LaTeX

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

Lean4

theorem local_compact_nhds [LocallyCompactSpace X] {x : X} {n : Set X} (h : n ∈ 𝓝 x) : ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s :=
  LocallyCompactSpace.local_compact_nhds _ _ h

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