uniformContinuous_coe

Mathlib.Topology.UniformSpace.AbstractCompletion

URI: https://scilib.ai/kg/mathlib#AbstractCompletion.uniformContinuous_coe

English

The coe map ι from α into its completion is uniformly continuous.

Русский

Пределение отображения включения ι из α в его дополнение является равномерно непрерывным.

LaTeX

$$$\\text{UniformContinuous}(\\iota)$$$

Lean4

theorem uniformContinuous_coe : UniformContinuous ι :=
  IsUniformInducing.uniformContinuous pkg.isUniformInducing

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

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

Разделы

Аффилиация

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