uniformContinuous_mul — Mathlib

English

On a bounded set s ⊆ ℝ×ℝ with bounds |x1|<r1, |x2|<r2, the product map is uniformly continuous.

Русский

На ограниченном подмножестве s ⊆ ℝ×ℝ с ограничениями |x1|<r1, |x2|<r2 отображение умножения непрерывно равномерно.

LaTeX

$$$\text{UniformContinuous}(p\mapsto p_1 p_2)$ для $p\in s$ с $|p_1|

Lean4

theorem uniformContinuous_mul (s : Set (ℝ × ℝ)) {r₁ r₂ : ℝ} (H : ∀ x ∈ s, |(x : ℝ × ℝ).1| < r₁ ∧ |x.2| < r₂) :
    UniformContinuous fun p : s => p.1.1 * p.1.2 :=
  Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abs ε0
    ⟨δ, δ0, fun {a b} h =>
      let ⟨h₁, h₂⟩ := max_lt_iff.1 h
      Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩

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