α : Type ?u.1048612
β : Type ?u.1048615
γ : Type ?u.1048618
γ₂ : Type ?u.1048621
δ : Type ?u.1048624
ι✝ : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
ι : Type u_1
π : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)
α : Type ?u.1048612
β : Type ?u.1048615
γ : Type ?u.1048618
γ₂ : Type ?u.1048621
δ : Type ?u.1048624
ι✝ : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
ι : Type u_1
π : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)
have : ‹∀ i, MeasurableSpace (π i)› = fun i => borel (π i) :=
  funext fun i => BorelSpace.measurable_eq
α : Type ?u.1048612
β : Type ?u.1048615
γ : Type ?u.1048618
γ₂ : Type ?u.1048621
δ : Type ?u.1048624
ι✝ : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
ι : Type u_1
π : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)
α : Type ?u.1048612
β : Type ?u.1048615
γ : Type ?u.1048618
γ₂ : Type ?u.1048621
δ : Type ?u.1048624
ι✝ : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
ι : Type u_1
π : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)
rw [this]
no goals
α : Type ?u.1048612
β : Type ?u.1048615
γ : Type ?u.1048618
γ₂ : Type ?u.1048621
δ : Type ?u.1048624
ι✝ : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
ι : Type u_1
π : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)
exact iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable