English
The distance on the completion is uniformly continuous in both arguments; i.e., the map (x,y) ↦ dist x y from Completion α × Completion α is uniformly continuous.
Русский
Расстояние на завершении является равномерно непрерывным по обеим аргументам; то есть отображение (x,y) ↦ dist x y: (Completion α) × (Completion α) → ℝ uniformly continuous.
LaTeX
$$$\text{UniformContinuous}\, (\lambda p: \mathrm{Completion}\;\alpha \times \mathrm{Completion}\;\alpha.\; \operatorname{dist} p.1 p.2)$$$
Lean4
/-- The new distance is uniformly continuous. -/
protected theorem uniformContinuous_dist : UniformContinuous fun p : Completion α × Completion α ↦ dist p.1 p.2 :=
uniformContinuous_extension₂ dist