case nil
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → Measurable f
hl : ∀ (f : α → M), f ∈ [] → Measurable f
⊢ Measurable (prod [])

case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → Measurable f_1
⊢ Measurable (prod (f :: l))
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → Measurable f
⊢ Measurable (prod l)
induction' l with f l ihl
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (prod (f :: l))
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → Measurable f_1
⊢ Measurable (prod (f :: l))
rw [List.forall_mem_cons] at hl
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (f * prod l)
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (prod (f :: l))
rw [List.prod_cons]
no goals
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (f * prod l)
exact hl.1.mul (ihl hl.2)
no goals
case nil
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → Measurable f
hl : ∀ (f : α → M), f ∈ [] → Measurable f
⊢ Measurable (prod [])
exact measurable_one