Erdős problem 602
Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?
Sources
FormalConjectures/ErdosProblems/
602.lean
Retained formal statement
Trivial case: pairwise disjoint families.
If the A_i are pairwise disjoint (all intersections are empty, which in particular satisfies |A_i ∩ A_j| ≠ 1), then Property B holds trivially.
Proof sketch: Since each A_i is infinite, it has (at least) two distinct elements a_i and b_i. We can define a colouring that assigns colour 0 to a_i and colour 1 to b_i for each i (using disjointness, these choices don't conflict), and extend arbitrarily elsewhere. Then no A_i is monochromatic.
True ↔ ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α), (∀ (i : I), (A i).Infinite) → (∀ (i j : I), i ≠ j → Disjoint (A i) (A j)) → Erdos602.HasPropertyB I ASolvedStatement only, no proof