UniformContinuous₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Uniform continuity for functions of two variables. -/
def UniformContinuous₂ (f : α → β → γ) :=
  UniformContinuous (uncurry f)

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