Q — Mathlib · SciLib

English

There is a uniform bijection between Bourbaki real numbers and the real numbers, i.e., a uniform isomorphism Bourbakiℝ ≃ᵤ ℝ.

Русский

Существуют униформные биекция между Bourbakiℝ и ℝ, т.е. униформное изоморфизм Bourbakiℝ ≃ᵤ ℝ.

LaTeX

$$$\text{CompareReals}.compareEquiv : Bourbaki\mathbb{R} \simeq_u \mathbb{R}$$$

Lean4

/-- Type wrapper around ℚ to make sure the absolute value uniform space instance is picked up
instead of the metric space one. We proved in `Rat.uniformSpace_eq` that they are equal,
but they are not definitionaly equal, so it would confuse the type class system (and probably
also human readers). -/
def Q :=
  ℚ
deriving CommRing, Inhabited

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