Erdős Problem 125

[DomonkosV]

fix #366

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[callesonne]

Thanks for the contribution! Looks good to me after these comments have been addressed :)

[callesonne]

Suggested change

	({ x : ℕ | (digits 3 x) ⊆ {0, 1} } + { x : ℕ | (digits 4 x) ⊆ {0, 1} }).HasPosDensity ↔
	{ x : ℕ | (digits 3 x).toFinset ⊆ {0, 1} } + { x : ℕ | (digits 4 x).toFinset ⊆ {0, 1} }.HasPosDensity ↔

Apparently here {0, 1} is treated as a list, because List has an instance of the Insert class, which is used to implement the notation { } for writing e.g. {a, b}. So the statement currently says that x has first digit 0 and second digit 1 (i.e. x = 3 or x = 4). I've suggested a fix.

[DomonkosV]

The round brackets are mandatory for .HasPosDensity to take the full set.

[callesonne]

Ah right, I forgot you were doing addition inside the brackets, my bad!

[callesonne]

Suggested change

	({ x : ℕ | (digits 3 x).toFinset ⊆ {0, 1} } + { x : ℕ | (digits 4 x).toFinset ⊆ {0, 1} }
	).HasPosDensity ↔ answer(sorry) := by
	theorem erdos_125 :
	({ x : ℕ | (digits 3 x).toFinset ⊆ {0, 1} } +
	{ x : ℕ | (digits 4 x).toFinset ⊆ {0, 1} }).HasPosDensity ↔ answer(sorry) := by

Final formatting suggestion :)

[callesonne]

Approved once this final formatting comment has been addressed :) Thanks a lot!