locallyCompactSpace — Mathlib

English

If L is locally compact, and the absolute value factors through an embedding into L, then the completion v.Completion is locally compact.

Русский

Если L локально компактно и величина v факторизуется через вложение в L, то дополнение v.Completion локально компактно.

LaTeX

$$$$\\text{LocallyCompactSpace}(v.Completion).$$$$

Lean4

/-- If the absolute value of a normed field factors through an embedding into another normed field
that is locally compact, then the completion of the first normed field is also locally compact. -/
theorem locallyCompactSpace [LocallyCompactSpace L] (h : ∀ x, ‖f x‖ = v x) : LocallyCompactSpace (v.Completion) :=
  (isClosedEmbedding_extensionEmbedding_of_comp h).locallyCompactSpace

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