uniformContinuous_add — Mathlib

English

Addition on ℚ is uniformly continuous: the map (p,q) ↦ p+q is uniformly continuous from ℚ×ℚ to ℚ.

Русский

Сложение в ℚ равномерно непрерывно: отображение (p,q) ↦ p+q из ℚ×ℚ в ℚ является равномерно непрерывным.

LaTeX

$$$\\operatorname{UniformContinuous}(+): \\mathbb{Q} \\times \\mathbb{Q} \ o \\mathbb{Q}$$$

Lean4

theorem uniformContinuous_add : UniformContinuous fun p : ℚ × ℚ => p.1 + p.2 :=
  Rat.isUniformEmbedding_coe_real.isUniformInducing.uniformContinuous_iff.2 <|
    by
    simp only [Function.comp_def, Rat.cast_add]
    exact Real.uniformContinuous_add.comp (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

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