uniformContinuous₂_def

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#uniformContinuous₂_def

English

A uniform continuous₂ function yields a uniformly continuous uncurry.

Русский

У функции UniformContinuous₂ имеется равномерная непрерывность для развертывания.

LaTeX

$$$UniformContinuous\₂ f \Rightarrow UniformContinuous(\text{uncurry } f)$$$

Lean4

theorem uniformContinuous₂_def (f : α → β → γ) : UniformContinuous₂ f ↔ UniformContinuous (uncurry f) :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru