α : Type u_1
β : Type u_2
γ : Type ?u.68690
ι : Type ?u.68693
inst✝³ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (mulSupport f)
α : Type u_1
β : Type u_2
γ : Type ?u.68690
ι : Type ?u.68693
inst✝³ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
⊢ MeasurableSet (mulSupport f)
borelize β
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.68690
ι : Type ?u.68693
inst✝³ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (mulSupport f)
exact measurableSet_mulSupport hf.measurable