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
Two infinite sets with pairwise intersection of size ≠ 1.
If the family consists of exactly two countably infinite sets A₀ and A₁ with |A₀ ∩ A₁| ≠ 1 (and finite), then Property B holds.
Proof sketch: - If A₀ ∩ A₁ = ∅: the sets are disjoint. Pick distinct a, b ∈ A₀ and distinct c, d ∈ A₁. Colour b and c with 1, everything else with 0. Then A₀ has a (colour 0) and b (colour 1), and A₁ has c (colour 1) and d (colour 0), so neither is monochromatic. - If |A₀ ∩ A₁| ≥ 2: the intersection contains two distinct points x and y. Assign x colour 0 and y colour 1. Both A₀ and A₁ contain x and y, so neither is monochromatic.
True ↔ ∀ {α : Type u_1} (A : Fin 2 → Set α), (∀ (i : Fin 2), (A i).Infinite) → (A 0 ∩ A 1).Finite → (A 0 ∩ A 1).ncard ≠ 1 → Erdos602.HasPropertyB (Fin 2) A