uncurry_right

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Continuous.uncurry_right

English

If uncurry f is continuous, then the map x ↦ f(x) is continuous for any fixed x.

Русский

Если uncurry f непрерывна, то для фиксированного x отображение y ↦ f(x,y) непрерывно.

LaTeX

$$Continuous (uncurry f) → Continuous (λ x, f x)$$

Lean4

theorem uncurry_right {f : X → Y → Z} (y : Y) (h : Continuous (uncurry f)) : Continuous fun a => f a y :=
  h.comp (.prodMk_left _)

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

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

Разделы

Аффилиация

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