uniformContinuous_dist — Mathlib

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

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