uniformSpace

Mathlib.Topology.UniformSpace.CompareReals

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

English

The uniform equivalence is compatible with the uniform structure on Bourbakiℝ and ℝ.

Русский

Униформное эквивалентное отображение согласовано с униформной структурой Bourbakiℝ и ℝ.

LaTeX

$$UniformEquiv.compareEquiv : Bourbakiℝ ≃ᵤ ℝ$$

Lean4

instance uniformSpace : UniformSpace Bourbakiℝ :=
  Completion.uniformSpace Q

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

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

Разделы

Аффилиация

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