α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | ¬essInf f μ ≤ f y} = 0
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | f y < essInf f μ} = 0
simp_rw [← not_le]
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | ¬essInf f μ ≤ f y} = 0
exact ae_essInf_le hf