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
Formal disproof of disjoint_without_infinite_claim.
Counterexample: Take α = ℕ, I = Fin 2, with A 0 = {0} and A 1 = {1}. These are pairwise disjoint, satisfying the only hypothesis. But singleton sets are vacuously monochromatic under any colouring: the only pair (x, y) ∈ {0} × {0} is (0, 0), and f 0 = f 0 trivially. So any colouring makes A 0 monochromatic, meaning HasPropertyB fails.
¬Erdos602.disjoint_without_infinite_claimSolvedStatement only, no proof