no goals
α : Type u_2
β : Type u_1
γ : Type ?u.64356
ι : Type ?u.64359
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ (x : α), x ∈ univᶜ → f x = 0
simp
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.64356
ι : Type ?u.64359
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ SigmaFinite (Measure.restrict μ univ)
rwa [Measure.restrict_univ]