Skip to content

Erdős problem 602

Start work

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

Empty index set.

If the index set I is empty (has no elements), then Property B holds vacuously: any 2-colouring works, since there are no sets to be made non-monochromatic.

FormalConjectures/ErdosProblems/602.leanErdos602.erdos_602.variants.empty_index2 linesExact file
∀ {α : Type u_1} (A : PEmpty.{u_2 + 1} → Set α),  (∀ (i : PEmpty.{u_2 + 1}), (A i).Infinite) → Erdos602.HasPropertyB PEmpty.{u_2 + 1} A
TextbookStatement only, no proof