uniformContinuous_ofMul

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#uniformContinuous_ofMul

English

The canonical map ofMul: α → Additive α is uniformly continuous.

Русский

Каноническое отображение ofMul: α → Additive α равно равномерно непрерывному.

LaTeX

$$$$\\UniformContinuous(\\mathrm{ofMul} : \\alpha \\to \\mathrm{Additive}\\ \\alpha).$$$$

Lean4

theorem uniformContinuous_ofMul : UniformContinuous (ofMul : α → Additive α) :=
  uniformContinuous_id

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

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

Разделы

Аффилиация

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