case nil
α : Type u_1
β : Type ?u.109795
γ : Type ?u.109798
ι : Type ?u.109801
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → StronglyMeasurable f
hl : ∀ (f : α → M), f ∈ [] → StronglyMeasurable f
⊢ StronglyMeasurable (List.prod [])

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