∀ {α : Type u_1} {mα : MeasurableSpace α} (φ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α),
  ProbabilityTheory.Kernel.IsIrreducible φ κ ↔
    ∀ ⦃A : Set α⦄, MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ n, ((κ ^ n) a) A > 0