isClosed_image_extensionEmbeddingOfIsReal

English

For a real infinite place, the image of the real extensionEmbedding is closed in ℝ.

Русский

Для вещественного места образ real extensionEmbedding замкнут в ℝ.

LaTeX

$$IsClosed (Set.range (extensionEmbeddingOfIsReal hv))$$

Lean4

/-- The embedding `v.Completion →+* ℝ` associated to a real infinite place has closed image
inside `ℝ`. -/
theorem isClosed_image_extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) :
    IsClosed (Set.range (extensionEmbeddingOfIsReal hv)) :=
  (isClosedEmbedding_extensionEmbedding_of_comp <| v.norm_embedding_of_isReal hv).isClosed_range

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