α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → β
⊢ sInf {a | ∀ᶠ (n : β) in map f (Measure.ae μ), n ≤ a} = sInf {a | ↑↑μ {x | a < f x} = 0}
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → β
⊢ essSup f μ = sInf {a | ↑↑μ {x | a < f x} = 0}
dsimp [essSup, limsup, limsSup]
no goals
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → β
⊢ sInf {a | ∀ᶠ (n : β) in map f (Measure.ae μ), n ≤ a} = sInf {a | ↑↑μ {x | a < f x} = 0}
simp only [eventually_map, ae_iff, not_le]