{Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} → [MeasurableSpace 𝓨] → (Θ → 𝓨 → ENNReal) → ProbabilityTheory.Kernel Θ 𝓧 → ENNReal