case nil
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)

case cons
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod l s)
induction' l with i l ih
case cons
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
case nil
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)

case cons
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
exact MeasurableSet.univ
no goals
case cons
α : Type ?u.373293
β : Type ?u.373296
γ : Type ?u.373299
δ : Type u_1
δ' : Type ?u.373305
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_2
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
exact (hs i).prod ih