uniformContinuous_compareEquiv_symm

Mathlib.Topology.UniformSpace.AbstractCompletion

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

English

The inverse of the comparison equivalence is uniformly continuous.

Русский

Обратное сравнение эквивалентности равномерно непрерывно.

LaTeX

$$$ UniformContinuous (pkg.compareEquiv pkg').symm $$$

Lean4

theorem uniformContinuous_compareEquiv_symm : UniformContinuous (pkg.compareEquiv pkg').symm :=
  pkg'.uniformContinuous_compare pkg

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

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

Разделы

Аффилиация

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