ι : Type ?u.311031
α : Type u_1
β : Type u_2
γ : Type ?u.311040
δ : Type ?u.311043
R : Type ?u.311046
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
✝ : Nontrivial α
⊢ AEMeasurable f
ι : Type ?u.311031
α : Type u_1
β : Type u_2
γ : Type ?u.311040
δ : Type ?u.311043
R : Type ?u.311046
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
⊢ AEMeasurable f
nontriviality α
ι : Type ?u.311031
α : Type u_1
β : Type u_2
γ : Type ?u.311040
δ : Type ?u.311043
R : Type ?u.311046
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
ι : Type ?u.311031
α : Type u_1
β : Type u_2
γ : Type ?u.311040
δ : Type ?u.311043
R : Type ?u.311046
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
✝ : Nontrivial α
⊢ AEMeasurable f
inhabit α
no goals
ι : Type ?u.311031
α : Type u_1
β : Type u_2
γ : Type ?u.311040
δ : Type ?u.311043
R : Type ?u.311046
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
exact ⟨fun _ => f default, measurable_const, rfl⟩