continuous_uncurry_of_continuous — Mathlib

English

The uncurried form of a continuous map X → C(Y,Z) is continuous X×Y → Z under LocallyCompact assumptions.

Русский

Неприкоснованная форма непрерывного отображения X → C(Y,Z) непрерывна X×Y → Z при локально компактном Y (и при необходимости X).

LaTeX

$$$\text{uncurry}:[LocallyCompactSpace Y] (f: C(X, C(Y,Z))) \to C(X\times Y, Z)$$ is continuous$$

Lean4

/-- The uncurried form of a continuous map `X → C(Y, Z)` is a continuous map `X × Y → Z`. -/
theorem continuous_uncurry_of_continuous [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :
    Continuous (Function.uncurry fun x y => f x y) :=
  continuous_eval.comp <| f.continuous.prodMap continuous_id

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