uniformContinuous_abs — Mathlib

English

The absolute value function on ℚ is uniformly continuous.

Русский

Функция абсолютной величины на ℚ равномерно непрерывна.

LaTeX

$$$\\operatorname{UniformContinuous}(|\\cdot|)$$$

Lean4

theorem uniformContinuous_abs : UniformContinuous (abs : ℚ → ℚ) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε, ε0, fun _ _ h => lt_of_le_of_lt (by simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩

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