uniformContinuous_inv

Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

English

The inverse map on a uniform group is uniformly continuous: x ↦ x^{-1} is uniformly continuous.

Русский

Обратная карта на равномерной группе равномерно непрерывна: x ↦ x^{-1}.

LaTeX

$$$\text{UniformContinuous inv}: \text{UniformContinuous } x \mapsto x^{-1}$.$$

Lean4

@[to_additive]
theorem uniformContinuous_inv : UniformContinuous fun x : α => x⁻¹ :=
  uniformContinuous_id.inv

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

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

Разделы

Аффилиация

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