compare_uc

Mathlib.Topology.UniformSpace.CompareReals

URI: https://scilib.ai/kg/mathlib#CompareReals.compare_uc

English

Uniform continuity of the symmetry of compareEquiv.

Русский

Равномерная непрерывность симметрии CompareEquiv.

LaTeX

$$$\text{UniformContinuous}(\text{CompareReals}.compareEquiv.symm)$$$

Lean4

theorem compare_uc : UniformContinuous compareEquiv :=
  bourbakiPkg.uniformContinuous_compareEquiv rationalCauSeqPkg

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

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

Разделы

Аффилиация

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