∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → ℚ),
      Monotone seq →
        Filter.Tendsto seq Filter.atTop Filter.atTop →
          ∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun m => f (a, c) (seq m)) Filter.atTop (nhds 1)