uniformContinuous_neg — Mathlib

English

Negation on ℚ is uniformly continuous: the map x ↦ -x is uniformly continuous.

Русский

Отрицание на ℚ равномерно непрерывно: отображение x ↦ -x равномерно непрерывно.

LaTeX

$$$\\operatorname{UniformContinuous}(-): \\mathbb{Q} \\to \\mathbb{Q}$$$

Lean4

theorem uniformContinuous_neg : UniformContinuous (@Neg.neg ℚ _) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩

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