True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, ∃ I, (∀ (i : Fin k), (I i).1 < (I i).2) ∧ (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧ ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1