Theorems · Definition · measure theory

MeasurableEquiv.piCongrLeft

{δ : Type u_4} →
  {δ' : Type u_5} →
    (π : δ' → Type u_6) →
      [inst : (x : δ') → MeasurableSpace (π x)] → (f : δ ≃ δ') → ((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)

Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

15 results in Mathlib

Foundations

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

Assumes

MeasurableSpace