Theorems · Definition · measure theory

MeasurableEquiv.piOptionEquivProd

{δ : Type u_8} →
  (α : Option δ → Type u_9) →
    [inst : (i : Option δ) → MeasurableSpace (α i)] → ((i : Option δ) → α i) ≃ᵐ ((i : δ) → α (some i)) × α none

The measurable equivalence for (dependent) functions on an Option type (∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace