isEmbedding_val

Mathlib.Topology.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#Units.isEmbedding_val

← MathLib Explorer

English

For any group G, the inclusion map val: Gˣ → G is a topological embedding.

Русский

Включение единиц группы Gˣ в G является топологическим вложением.

LaTeX

$$$ IsEmbedding (\\text{val} : G^{\\times} \\to G) $$$

Lean4

@[to_additive]
theorem isEmbedding_val [Group G] [TopologicalSpace G] [ContinuousInv G] : IsEmbedding (val : Gˣ → G) :=
  toUnits_homeomorph.symm.isEmbedding

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

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

Разделы

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

Аффилиация

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