extensionEmbeddingOfIsReal_coe — Mathlib

English

The image of extensionEmbedding is a closed subset of the ambient field (ℂ or ℝ depending on real/complex place).

Русский

Образ extensionEmbedding замкнут в ℂ (или ℝ для вещественных мест).

LaTeX

$$IsClosed (Set.range (extensionEmbedding v))$$

Lean4

@[simp]
theorem extensionEmbeddingOfIsReal_coe {v : InfinitePlace K} (hv : IsReal v) (x : K) :
    extensionEmbeddingOfIsReal hv x = embedding_of_isReal hv x :=
  extensionEmbedding_of_comp_coe (v.norm_embedding_of_isReal hv) x

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