uniformContinuous_toAdd

Mathlib.Topology.UniformSpace.Basic

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

English

Uniform continuity of toAdd: Multiplicative α → α.

Русский

Равномерная непрерывность toAdd: Multiplicative α → α.

LaTeX

$$$$\\UniformContinuous(\\mathrm{toAdd} : \\mathrm{Multiplicative}\\ \\alpha \\to \\alpha).$$$$

Lean4

theorem uniformContinuous_toAdd : UniformContinuous (toAdd : Multiplicative α → α) :=
  uniformContinuous_id

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

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

Разделы

Аффилиация

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