prodMk — Mathlib

English

If f1 and f2 are uniformly continuous, then the map a ↦ (f1(a), f2(a)) is uniformly continuous.

Русский

Если f1 и f2 равномерно непрерывны, то отображение a ↦ (f1(a), f2(a)) равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous}~f_1 \to \text{UniformContinuous}~f_2 \Rightarrow \text{UniformContinuous}(\lambda a. (f_1(a), f_2(a)))$$$

Lean4

theorem prodMk {f₁ : α → β} {f₂ : α → γ} (h₁ : UniformContinuous f₁) (h₂ : UniformContinuous f₂) :
    UniformContinuous fun a => (f₁ a, f₂ a) :=
  by
  rw [UniformContinuous, uniformity_prod]
  exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

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