True ↔ Filter.limsup (fun k => (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) - ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) / ↑(Real.log (↑k + 1))) Filter.atTop = ⊤