α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
⊢ essSup (fun x => c) μ ≤ c
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
⊢ essSup f μ ≤ c
refine' (essSup_mono_ae hf).trans _
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : μ = 0
⊢ essSup (fun x => c) μ ≤ c

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : ¬μ = 0
⊢ essSup (fun x => c) μ ≤ c
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
⊢ essSup (fun x => c) μ ≤ c
by_cases hμ : μ = 0
no goals
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : μ = 0
⊢ essSup (fun x => c) μ ≤ c
simp [hμ]
no goals
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : ¬μ = 0
⊢ essSup (fun x => c) μ ≤ c
rwa [essSup_const]