erdos_1071a

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

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.