uniformContinuous — Mathlib

English

The uniform continuity of a binary function implies the uniform continuity of its uncurry form.

Русский

Равномерная непрерывность бинарной функции влечёт равномерную непрерывность её раскрученной формы.

LaTeX

$$$uniformContinuous\₂ f \to uniformContinuous(uncurry f)$$$

Lean4

theorem uniformContinuous {f : α → β → γ} (h : UniformContinuous₂ f) : UniformContinuous (uncurry f) :=
  h

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