False ↔ ∀ (A B : Set ℕ), ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count A n)) → ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count B n)) → {(a₁, a₂, b₁, b₂) | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite