Skip to content

Erdős problem 774

Is every proportionately dissociated (infinite) set the union of a finite number of dissociated sets?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

774.lean

Retained formal statement1 of 1

Is every proportionately dissociated (infinite) set the union of a finite number of dissociated sets?

FormalConjectures/ErdosProblems/774.leanErdos774.erdos_7742 linesExact file
True ↔  ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated → ∃ T, (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T
OpenStatement only, no proof