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 statement2 of 8

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.

FormalConjectures/ErdosProblems/602.leanErdos602.erdos_6025 linesExact file
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
OpenStatement only, no proof