Skip to content

Erdős problem 602

Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

602.lean

Retained formal statement4 of 8

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.

FormalConjectures/ErdosProblems/602.leanErdos602.erdos_602.variants.disjoint3 linesExact file
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 A
SolvedStatement only, no proof