uniformContinuous₂_curry — Mathlib

English

Let f: α × β → γ be a function between uniform spaces. Then f is uniformly continuous in two variables if and only if its curry version curry f: α → β → γ is uniformly continuous.

Русский

Пусть f: α × β → γ — функция между равномерными пространствами. Тогда f является равномерно непрерывной по двум аргументам тогда и только тогда, когда её карри-версия curry f: α → β → γ равномерно непрерывна.

LaTeX

$$$\\operatorname{UniformContinuous}_2(\\operatorname{curry}(f)) \\iff \\operatorname{UniformContinuous}(f)$$$

Lean4

theorem uniformContinuous₂_curry (f : α × β → γ) : UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f := by
  rw [UniformContinuous₂, uncurry_curry]

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