Documentation

GibbsMeasure.Mathlib.MeasureTheory.MeasurableSpace.Basic

theorem MeasureTheory.measurable_one' {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} [One α] :
theorem MeasureTheory.measurable_zero' {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} [Zero α] :