Theorems · Definition · measure theory

MeasurableEquiv.piFinsetUnion

{δ' : Type u_5} →
  (π : δ' → Type u_6) →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      [inst_1 : DecidableEq δ'] →
        {s t : Finset δ'} → Disjoint s t → ((i : ↥s) → π ↑i) × ((i : ↥t) → π ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → π ↑i)

The measurable equivalence (∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i) for disjoint finsets s and t. Equiv.piFinsetUnion as a measurable equivalence.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEq