outCLM_isUniformEmbedding

Mathlib.Topology.Algebra.SeparationQuotient.Section

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

← MathLib Explorer

English

The map outCLM K E is a uniform embedding.

Русский

Отображение outCLM K E является равномерно вложением.

LaTeX

$$$\mathrm{IsUniformEmbedding}(\mathrm{outCLM}_{K,E})$$$

Lean4

theorem outCLM_isUniformEmbedding : IsUniformEmbedding (outCLM K E)
    where
  injective := outCLM_injective K E
  toIsUniformInducing := outCLM_isUniformInducing K E

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

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

Разделы

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

Аффилиация

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