Theorems · Definition · measure theory

MeasurableEquiv.piEquivPiSubtypeProd

{δ' : Type u_5} →
  (π : δ' → Type u_6) →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      (p : δ' → Prop) → [DecidablePred p] → ((i : δ') → π i) ≃ᵐ ((i : Subtype p) → π ↑i) × ((i : { i // ¬p i }) → π ↑i)

Measurable equivalence between (dependent) functions on a type and pairs of functions on {i // p i} and {i // ¬p i}. See also Equiv.piEquivPiSubtypeProd.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidablePred