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
Retained formal statement
Countable index set case.
If the index set is countable, the answer is yes, and the intersection condition is unnecessary. This is Bernstein's Lemma: every countable system of infinite sets has Property B.
True ↔ ∀ {α : Type u_1} (A : ℕ → Set α), (∀ (i : ℕ), (A i).Countable ∧ (A i).Infinite) → (∀ (i j : ℕ), i ≠ j → (A i ∩ A j).Finite) → (∀ (i j : ℕ), i ≠ j → (A i ∩ A j).ncard ≠ 1) → Erdos602.HasPropertyB ℕ ASolvedStatement only, no proof