True ↔ ∀ (a : ℕ → ℕ), (∀ (i : ℕ), 0 < a i) → StrictMono a → (∃ i, a i ≠ Erdos315.u i + 1) → ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c₀