Theorems · Theorem · measure theory

MeasurableEquiv.piEquivPiSubtypeProd_symm_apply

∀ {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] (p : δ' → Prop)
  [inst_1 : DecidablePred p],
  ⇑(MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun f x => if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidablePred