Erdős Problem 197

Reference: erdosproblems.com/197

theorem Erdos197.erdos_197 : sorry ↔ ∃ (A : Set ℕ) (B : Set ℕ), IsCompl A B ∧ (∃ (f : ℕ ≃ ↑A), ¬HasMonotoneAP (Subtype.val ∘ ⇑f) 3) ∧ ∃ (g : ℕ ≃ ↑B), ¬HasMonotoneAP (Subtype.val ∘ ⇑g) 3

Can $\mathbb{N}$ be partitioned into two sets, each of which can be permuted to avoid monotone 3-term arithmetic progressions?