Erdős Problem 1071

References:

• erdosproblems.com/1071
• [Da85] Danzer, L., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985), 167-177.

def Erdos1071.SegmentsDisjoint (seg1 seg2 : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)) : Prop

Two segments are disjoint if they only intersect at their endpoints (if at all).

Equations

• Erdos1071.SegmentsDisjoint seg1 seg2 = (segment ℝ seg1.1 seg1.2 ∩ segment ℝ seg2.1 seg2.2 ⊆ {seg1.1, seg1.2, seg2.1, seg2.2})

theorem Erdos1071.erdos_1071a : True ↔ ∃ (S : Finset (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2))), (∀ seg ∈ S, dist seg.1 seg.2 = 1 ∧ seg.1 0 ∈ Set.Icc 0 1 ∧ seg.1 1 ∈ Set.Icc 0 1 ∧ seg.2 0 ∈ Set.Icc 0 1 ∧ seg.2 1 ∈ Set.Icc 0 1) ∧ (↑S).Pairwise SegmentsDisjoint ∧ Maximal (fun (T : Finset (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2))) => (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1 0 ∈ Set.Icc 0 1 ∧ seg.1 1 ∈ Set.Icc 0 1 ∧ seg.2 0 ∈ Set.Icc 0 1 ∧ seg.2 1 ∈ Set.Icc 0 1) ∧ (↑T).Pairwise SegmentsDisjoint) S

Can a finite set of disjoint unit segments in a unit square be maximal? Solved affirmatively by [Da85], who gave an explicit construction.

theorem Erdos1071.erdos_1071b : sorry ↔ ∃ (R : Set (EuclideanSpace ℝ (Fin 2))) (S : Set (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2))), S.Countable ∧ S.Infinite ∧ Maximal (fun (T : Set (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2))) => (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1 ∈ R ∧ seg.2 ∈ R) ∧ T.Pairwise SegmentsDisjoint) S

Is there a region $R$ with a maximal set of disjoint unit line segments that is countably infinite?