case nil
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
hl : ∀ (f : α → M), f ∈ [] → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (List.prod []) μ

case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable (List.prod (f :: l)) μ
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (List.prod l) μ
induction' l with f l ihl
case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : AEStronglyMeasurable f μ ∧ ∀ (x : α → M), x ∈ l → AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (List.prod (f :: l)) μ
case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable (List.prod (f :: l)) μ
rw [List.forall_mem_cons] at hl
case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : AEStronglyMeasurable f μ ∧ ∀ (x : α → M), x ∈ l → AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * List.prod l) μ
case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : AEStronglyMeasurable f μ ∧ ∀ (x : α → M), x ∈ l → AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (List.prod (f :: l)) μ
rw [List.prod_cons]
no goals
case cons
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEStronglyMeasurable f μ
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ) → AEStronglyMeasurable (List.prod l) μ
hl : AEStronglyMeasurable f μ ∧ ∀ (x : α → M), x ∈ l → AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * List.prod l) μ
exact hl.1.mul (ihl hl.2)
no goals
case nil
α : Type u_1
β : Type ?u.310152
γ : Type ?u.310155
ι : Type ?u.310158
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
hl : ∀ (f : α → M), f ∈ [] → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (List.prod []) μ
exact aestronglyMeasurable_one