English
Define an abstract completion of ℚ via the absolute value uniformity, yielding a completion object isomorphic to the real numbers.
Русский
Определяем абстрактное дополнение к ℚ через униформность по модулю, получая завершение, изоморфное вещественным числам.
LaTeX
$$def rationalCauSeqPkg : AbstractCompletion ℚ (abs.uniformSpace) := …$$
Lean4
/-- Cauchy reals packaged as a completion of ℚ using the absolute value route. -/
def rationalCauSeqPkg : @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).uniformSpace :=
@AbstractCompletion.mk (space := ℝ) (coe := ((↑) : ℚ → ℝ)) (uniformStruct := by infer_instance) (complete := by
infer_instance) (separation := by infer_instance) (isUniformInducing :=
by
rw [Rat.uniformSpace_eq]
exact Rat.isUniformEmbedding_coe_real.isUniformInducing) (dense := Rat.isDenseEmbedding_coe_real.dense)
