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
Intersections of size ≥ 2 suffice.
For a single countably infinite set A ⊆ α, there trivially exists a 2-colouring of α that makes A non-monochromatic: since A is infinite, it has two distinct elements, so any colouring that assigns them different colours works.
∀ {α : Type u_1} (A : Set α), A.Infinite → ∃ f, ¬Erdos602.IsMonochromatic f ATextbookStatement only, no proof