This module additional Measurable lemmas for Sigma types.

@[simp]

theorem MeasurableSpace.Sigma.measurable_iff {A : Type u_1} {I : Type u_2} {P : I → Type u_3} [MeasurableSpace A] [(i : I) → MeasurableSpace (P i)] {f : Sigma P → A} : Measurable f ↔ ∀ (i : I), Measurable fun (x : P i) => f ⟨i, x⟩

@[simp]

theorem MeasurableSpace.Sigma.measurable_mk {I : Type u_2} {P : I → Type u_3} [(i : I) → MeasurableSpace (P i)] (i : I) : Measurable (Sigma.mk i)

theorem MeasurableSpace.Sigma.measurable_fst {I : Type u_2} {P : I → Type u_3} [(i : I) → MeasurableSpace (P i)] [MeasurableSpace I] : Measurable Sigma.fst

theorem MeasurableSpace.Sigma.measurable_cast {A : Type u_1} {I : Type u_2} {P : I → Type u_3} [MeasurableSpace A] [(i : I) → MeasurableSpace (P i)] (ix : A → I) (i : I) (p : ∀ (x : A), ix x = i) (f : (x : A) → P (ix x)) (hf : Measurable fun (x : A) => ⟨ix x, f x⟩) : Measurable fun (x : A) => cast ⋯ (f x)

theorem MeasurableSpace.Sigma.measurable_eq_rec {A : Type u_1} {I : Type u_2} {P : I → Type u_3} [MeasurableSpace A] [(i : I) → MeasurableSpace (P i)] (ix : A → I) (i : I) (p : ∀ (x : A), ix x = i) (f : (x : A) → P (ix x)) (hf : Measurable fun (x : A) => ⟨ix x, f x⟩) : Measurable fun (x : A) => ⋯ ▸ f x