Erdős Problem 846

Reference: erdosproblems.com/846

def Erdos846.NonTrilinearFor (A : Set (EuclideanSpace ℝ (Fin 2))) (ε : ℝ) : Prop

We say a subset A of points in the plane is ε-non-trilinear if any subset B of A, contains a non-trilinear subset C of size at least ε|B|.

Equations

• Erdos846.NonTrilinearFor A ε = ∀ (B : Finset (EuclideanSpace ℝ (Fin 2))), ↑B ⊆ A → ∃ C ⊆ B, ε * ↑B.card ≤ ↑C.card ∧ EuclideanGeometry.NonTrilinear ↑C

def Erdos846.WeaklyNonTrilinear (A : Set (EuclideanSpace ℝ (Fin 2))) : Prop

We say a subset A of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets.

Equations

• Erdos846.WeaklyNonTrilinear A = ∃ (B : Finset (Set (EuclideanSpace ℝ (Fin 2)))), A = sSup ↑B ∧ ∀ b ∈ B, EuclideanGeometry.NonTrilinear b

theorem Erdos846.erdos_846 : (∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → NonTrilinearFor A ε → WeaklyNonTrilinear A) ↔ sorry

Erdős Problem 846 Let A ⊂ ℝ² be an infinite set for which there exists some ϵ>0 such that in any subset of A of size n there are always at least ϵn with no three on a line. Is it true that A is the union of a finite number of sets where no three are on a line?

In other words, prove or disprove the following statement: every infinite ε-non-trilinear subset of the plane is weakly non-trilinar.