Theorems · Definition · general topology

ContinuousMap.curry

{X : Type u_2} →
  {Y : Type u_3} →
    {Z : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → C(X × Y, Z) → C(X, C(Y, Z))

The curried form of a continuous map α × β → γ as a continuous map α → C(β, γ). If a × β is locally compact, this is continuous. If α and β are both locally compact, then this is a homeomorphism, see Homeomorph.curry.

Defined in

Mathlib.Topology.CompactOpen

Cited by

26 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace