Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. Let x↦F(x)x\mapsto F(x) assign to every real xx a closed set F(x)⊆RF(x)\subseteq\mathbb R of Lebesgue measure less than 11. Then there is an infinite set X⊆RX\subseteq\mathbb R with x∉F(y)x\notin F(y) for all distinct x,y∈Xx,y\in X (Corollary (1), p. 338, of the Theorem on p. 336). No boundedness is assumed. An infinite independent set contains one of size 33, so the second question of Problem 501 has a positive answer; the paper presents the corollary as the answer to Problem 38(B) of the Erdős–Hajnal list. Gładysz had earlier found a free pair under an integral condition on the sets, as the paper describes it on p. 335 (the site states his result under the second question's hypotheses; Acta Math. Acad. Sci. Hungar. 13 (1962), 199–201; not held).

Covers. The second question only: closed sets AxA_x of measure <1<1 force an independent set of size 33, and in fact an infinite one. The first question, about bounded sets of outer measure <1<1 that need not be closed, lies outside the Theorem's closed-sections hypothesis and is settled on Glazer's claim page.

Source. L. Newelski, J. Pawlikowski and W. Seredyński, Infinite free set for small measure set mappings, Proc. Amer. Math. Soc. 100 (1987), no. 2, 335–339, received by the editors 1986-01-06. Its Lemma, Theorem and Corollaries (1)–(4) are recorded clause by clause on the source card, the proofs followed and not verified. This page is dated by the issue month, June 1987; the issue prints no day.

Acceptance. Refereed: the Proceedings of the American Mathematical Society. Reviewed: the curator of erdosproblems.com (T. F. Bloom) credits [NPS87] in the problem's commentary with an infinite independent set under the second question's hypotheses, and so with the answer to that question; the page's label NOT DISPROVABLE composes this part with the independence of the first question. The curator is independent of the authors.

Formalization. The conclusion is proved in Lean, from Mathlib, as erdos501_closed_infinite, and the question as asked (an independent set of size at least 33) as erdos501_closed_size3, inside Glazer's development, whose comparator targets state this theorem under the authors' names; the development and the copy of it in Boris Alexeev's repository are linked above at their pinned commits, and formal-conjectures 501.lean marks its variants closed_size3 and newelski_pawlikowski_seredynski research solved with formal-proof links to that copy. The development's own axiom audit and comparator record are described on Glazer's claim page. Neither copy was built in this corpus, so the formalization is a link and not formalized evidence.