uniformContinuous_add — Mathlib

English

The map (x,y) ↦ x+y on R×R is uniformly continuous.

Русский

Отображение (x,y) ↦ x+y из \\mathbb{R}×\\mathbb{R} в \\mathbb{R} является равномерно непрерывным.

LaTeX

$$$ UniformContinuous( (x,y) \mapsto x+y ) $$$

Lean4

theorem uniformContinuous_add : UniformContinuous fun p : ℝ × ℝ => p.1 + p.2 :=
  Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0
    ⟨δ, δ0, fun _ _ h =>
      let ⟨h₁, h₂⟩ := max_lt_iff.1 h
      Hδ h₁ h₂⟩

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