prodMap — Mathlib

English

If f and g are uniform continuous, then the map p ↦ (f(p.1), g(p.2)) is uniformly continuous.

Русский

Если f и g равномерно непрерывны, то отображение p ↦ (f(p.1), g(p.2)) равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous}(f) \to \text{UniformContinuous}(g) \Rightarrow \text{UniformContinuous}(\lambda p. (f(p.1), g(p.2)))$$$

Lean4

theorem prodMap [UniformSpace δ] {f : α → γ} {g : β → δ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
    UniformContinuous (Prod.map f g) :=
  (hf.comp uniformContinuous_fst).prodMk (hg.comp uniformContinuous_snd)

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