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
Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?
Formally: let α be any type, let (A_i)_{i ∈ I} be a family of countably infinite subsets of α such that for all i ≠ j, the intersection A_i ∩ A_j is finite and |A_i ∩ A_j| ≠ 1. Does there exist a 2-colouring f : α → Fin 2 such that no A_i is monochromatic?
This is an open question about Property B for almost-disjoint families with a forbidden intersection size of 1.
Note: This generalises the formulation in which the ground set is ℕ. Since every countably infinite set is in bijection with ℕ, the two formulations are equivalent, but working over an arbitrary ground type makes the statement apply immediately to, e.g., almost-disjoint families of countable subsets of an uncountable space.
True ↔ ∀ {α : Type u_1} {I : Type u_2} (A : I → Set α), (∀ (i : I), (A i).Countable ∧ (A i).Infinite) → (∀ (i j : I), i ≠ j → (A i ∩ A j).Finite) → (∀ (i j : I), i ≠ j → (A i ∩ A j).ncard ≠ 1) → Erdos602.HasPropertyB I A