theorem essSup_le_iSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] {f : α → β} : essSup f μ ≤ ⨆ (i : α), f i

theorem iSup_le_essSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLinearOrder β] {f : α → β} (h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y : α | a < f y} ≠ 0) : ⨆ (x : α), f x ≤ essSup f μ