α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLattice β
c : β
hμ : NeBot (Measure.ae μ)
⊢ essSup (fun x => c) μ = c
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLattice β
c : β
hμ : μ ≠ 0
⊢ essSup (fun x => c) μ = c
rw [← ae_neBot] at hμ
no goals
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : ConditionallyCompleteLattice β
c : β
hμ : NeBot (Measure.ae μ)
⊢ essSup (fun x => c) μ = c
exact essSup_const' _