Erdős Problem 846

Reference: erdosproblems.com/846

def Triplewise {α : Type u_1} (s : Set α) (r : α → α → α → Prop) : Prop

Equations

• Triplewise s r = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ∀ ⦃z : α⦄, z ∈ s → x ≠ y → y ≠ z → x ≠ z → r x y z

def NonTrilinear (A : Set (EuclideanSpace ℝ (Fin 2))) : Prop

We say a subset A of points in the plane is non-trilinear if it contains no three points that lie on the same line.

Equations

• NonTrilinear A = ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, Triplewise A fun (x y z : EuclideanSpace ℝ (Fin 2)) => ¬Collinear ℝ {x, y, z}

def 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

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

def 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

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

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

Euler 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.