expMapBasis_closure_subset_compactSet

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet

← MathLib Explorer

English

The image expMapBasis''closure(paramSet(K)) lies inside the compactSet(K).

Русский

Образ expMapBasis''closure(paramSet(K)) содержится в compactSet(K).

LaTeX

$$$\\expMapBasis''\\overline{\\operatorname{paramSet}(K)} \\subseteq \\operatorname{compactSet}(K)$$$

Lean4

theorem expMapBasis_closure_subset_compactSet : expMapBasis '' closure (paramSet K) ⊆ compactSet K :=
  by
  rw [compactSet_eq_union]
  exact Set.subset_union_left

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

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

Разделы

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

Аффилиация

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