uniformContinuous_dist — Mathlib

English

The map sending a pair of points to their distance is uniformly continuous: p ↦ dist(p1,p2) is UniformContinuous.

Русский

Отображение пары точек в их расстояние равномерно непрерывно: p ↦ dist(p1,p2).

LaTeX

$$$\text{UniformContinuous}(\lambda p:\nobreak (\alpha\times\alpha),\, \operatorname{dist}(p_1,p_2))$$$

Lean4

theorem uniformContinuous_dist : UniformContinuous fun p : α × α => dist p.1 p.2 :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε / 2, half_pos ε0, fun {a b} h =>
      calc
        dist (dist a.1 a.2) (dist b.1 b.2) ≤ dist a.1 b.1 + dist a.2 b.2 := dist_dist_dist_le _ _ _ _
        _ ≤ dist a b + dist a b := (add_le_add (le_max_left _ _) (le_max_right _ _))
        _ < ε / 2 + ε / 2 := (add_lt_add h h)
        _ = ε := add_halves ε⟩

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