False ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (A : Set ℕ), A.Infinite → (∀ (N : ℕ), (A ∩ Set.Icc 1 N).ncard ≤ f N) → (∀ (p : ℕ), Nat.Prime p → ∃ b, ∀ a ∈ A, ↑a ≠ b) → ∃ n, ∀ a ∈ A, Nat.Prime (n + a)