outCLM_uniformContinuous

Mathlib.Topology.Algebra.SeparationQuotient.Section

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

English

The map outCLM K E is uniformly continuous.

Русский

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

LaTeX

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

Lean4

theorem outCLM_uniformContinuous : UniformContinuous (outCLM K E) :=
  (outCLM_isUniformInducing K E).uniformContinuous

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

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

Разделы

Аффилиация

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