isEmbedding_outCLM

Mathlib.Topology.Algebra.SeparationQuotient.Section

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.isEmbedding_outCLM

← MathLib Explorer

English

The outCLM map is a topological embedding.

Русский

Карта outCLM является топологическим вложением.

LaTeX

$$$\text{IsEmbedding}(\mathrm{outCLM}\,K\,E)$$$

Lean4

/-- The `SeparationQuotient.outCLM K E` map is a topological embedding. -/
theorem isEmbedding_outCLM : IsEmbedding (outCLM K E) :=
  Function.LeftInverse.isEmbedding (mk_outCLM K) continuous_mk (map_continuous _)

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

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

Разделы

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

Аффилиация

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