continuous_curry

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#continuous_curry

English

If g: X × Y → Z is continuous at (x,y), then curry g x is continuous at y, and also uncurry_left relates them.

Русский

Если g: X × Y → Z непрерывна в (x,y), то curry g x непрерывна в y.

LaTeX

$$Continuous g → Continuous (curry g x)$$

Lean4

theorem continuous_curry {g : X × Y → Z} (x : X) (h : Continuous g) : Continuous (curry g x) :=
  Continuous.uncurry_left x h

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

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

Разделы

Аффилиация

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