@[simp]

theorem List.Encoding.measurable_cons {A : Type u_1} [MeasurableSpace A] : Measurable fun (x : A × Encoding A) => cons x.1 x.2

theorem List.Encoding.measurable_fold {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] {cons : A → B → B} (hcons : Measurable fun (x : A × B) => match x with | (x, y) => cons x y) (nil : B) : Measurable (foldr cons nil)

instance MeasureTheory.List.instMeasurableSpaceList_quasiBorelSpaces {A : Type u_1} [MeasurableSpace A] : MeasurableSpace (List A)

Equations

• MeasureTheory.List.instMeasurableSpaceList_quasiBorelSpaces = MeasurableSpace.comap List.Encoding.encode inferInstance

theorem MeasureTheory.List.measurable_encode {A : Type u_1} [MeasurableSpace A] : Measurable List.Encoding.encode

theorem MeasureTheory.List.measurable_to_encode {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] (f : A → List B) : Measurable f ↔ Measurable fun (x : A) => List.Encoding.encode (f x)

@[simp]

theorem MeasureTheory.List.measurable_cons {A : Type u_1} [MeasurableSpace A] : Measurable fun (x : A × List A) => match x with | (x, xs) => x :: xs

theorem MeasureTheory.List.measurable_cons' {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] {f : A → B} (hf : Measurable f) {g : A → List B} (hg : Measurable g) : Measurable fun (x : A) => f x :: g x

theorem MeasureTheory.List.measurable_foldr {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] {cons : A → B → B} (hcons : Measurable fun (x : A × B) => match x with | (x, xs) => cons x xs) (nil : B) : Measurable (List.foldr cons nil)

instance MeasureTheory.List.instDiscreteMeasurableSpaceListOfCountable_quasiBorelSpaces {A : Type u_1} [MeasurableSpace A] [DiscreteMeasurableSpace A] [Countable A] : DiscreteMeasurableSpace (List A)