Theorems · Definition · measure theory

MeasurableEquiv.piCurry

{ι : Type u_6} →
  {κ : ι → Type u_7} →
    (X : (i : ι) → κ i → Type u_8) →
      [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)] →
        ((p : (i : ι) × κ i) → X p.fst p.snd) ≃ᵐ ((i : ι) → (j : κ i) → X i j)

The currying operation Function.curry as a measurable equivalence. See MeasurableEquiv.curry for the non-dependent version.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

8 results in Mathlib

Foundations

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

Assumes

MeasurableSpace