erdos_1071b

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

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

Recent Submissions

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