α : Type ?u.149199
β : Type ?u.149202
γ : Type u_1
γ₂ : Type ?u.149208
δ : Type u_2
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
α : Type ?u.149199
β : Type ?u.149202
γ : Type u_1
γ₂ : Type ?u.149208
δ : Type u_2
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
rw [‹BorelSpace γ›.measurable_eq]
no goals
α : Type ?u.149199
β : Type ?u.149202
γ : Type u_1
γ₂ : Type ?u.149208
δ : Type u_2
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
exact measurable_generateFrom hf