Theorems · Theorem · measure theory

essInf_eq_sSup

∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → β), essInf f μ = sSup {a | μ {x | f x < a} = 0}

Defined in

Mathlib.MeasureTheory.Function.EssSup

Cited by

0 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLinearOrder