uniformContinuous_div

Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

English

The division map on a uniform group is uniformly continuous.

Русский

Операция деления в равномерной группе является равномерно непрерывной.

LaTeX

$$$\uniformContinuous\_div : (G\times G) \to G$ is uniformly continuous.$$

Lean4

@[to_additive]
theorem uniformContinuous_div : UniformContinuous fun p : α × α => p.1 / p.2 :=
  IsUniformGroup.uniformContinuous_div

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

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

Разделы

Аффилиация

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