case inl
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f

case inr
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f
rcases eq_or_ne μ 0 with (rfl | hμ)
no goals
case inl
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f
exact aemeasurable_zero_measure
case inr
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
⊢ AEMeasurable f
case inr
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f
haveI := ae_neBot.2 hμ
case inr.intro
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f
case inr
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
⊢ AEMeasurable f
rcases h.exists with ⟨x, hx⟩
no goals
case inr.intro
ι : Type ?u.3045534
α : Type u_1
β : Type u_2
γ : Type ?u.3045543
δ : Type ?u.3045546
R : Type ?u.3045549
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f
exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩