isClosed_image_extensionEmbedding

Mathlib.NumberTheory.NumberField.InfinitePlace.Completion

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding

← MathLib Explorer

English

The image of extensionEmbedding is closed in ℂ for a given v.

Русский

Образ extensionEmbedding замкнут в ℂ.

LaTeX

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

Lean4

/-- The embedding `v.Completion →+* ℂ` has closed image inside `ℂ`. -/
theorem isClosed_image_extensionEmbedding : IsClosed (Set.range (extensionEmbedding v)) :=
  (isClosedEmbedding_extensionEmbedding_of_comp v.norm_embedding_eq).isClosed_range

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru