Bourbakiℝ

Mathlib.Topology.UniformSpace.CompareReals

URI: https://scilib.ai/kg/mathlib#CompareReals.Bourbakiℝ

English

The inverse of compareEquiv is also uniformly continuous.

Русский

Обратная к compareEquiv функция также равномерно непрерывна.

LaTeX

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

Lean4

/-- Real numbers constructed as in Bourbaki. -/
def Bourbakiℝ : Type :=
  Completion Q
deriving Inhabited

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

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

Разделы

Аффилиация

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