α : Type u_1
β : Type u_2
γ : Type ?u.905162
δ : Type ?u.905165
m : MeasurableSpace α
inst✝² : Zero β
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y})
α : Type u_1
β : Type u_2
γ : Type ?u.905162
δ : Type ?u.905165
m : MeasurableSpace α
inst✝² : Zero β
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ↑f)
rw [f.support_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.905162
δ : Type ?u.905165
m : MeasurableSpace α
inst✝² : Zero β
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y})
exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _