Documentation

GibbsMeasure.Mathlib.MeasureTheory.Measure.AEMeasurable

theorem AEMeasurable.measurable {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [μ.IsComplete] :

Alias of the forward direction of aemeasurable_iff_measurable.