OAI/Combinatorics/CompleteCrossing/Polygonalization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Admissible polygonal replacement and retention of crossing counts.

  1. def OAI.Paper170Geometry.DrawingPassages.crossingDisk line 20
  2. theorem OAI.Paper170Geometry.DrawingPassages.crossingDisk_isOpen line 23
  3. theorem OAI.Paper170Geometry.DrawingPassages.crossingDisk_subset_closed line 28
  4. theorem OAI.Paper170Geometry.DrawingPassages.crossingDisk_disjoint_vertex_disk line 33
  5. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_openTrace_iff line 41
  6. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_range_in_crossingDisk line 73
  7. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_trace_in_crossingDisk line 97
  8. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_meeting_proper line 140
  9. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossings_proper line 166
  10. def OAI.Paper170Geometry.PolygonalExterior.assembledAdmissible line 194
  11. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossingCount_le line 204
  12. theorem OAI.Paper170Geometry.PolygonalExterior.middlePath_hasFiniteAffineCover line 236
  13. theorem OAI.Paper170Geometry.PolygonalExterior.assembledEdge_hasFiniteAffineCover line 241
  14. theorem OAI.Paper170Geometry.finite_intersection_normalization line 253

    Source documentation

    Finite contacts and no triples suffice to construct genuinely proper crossings.

    theorem finite_intersection_normalization [Fintype Vertex] [Fintype Edge] (D : FiniteIntersectionDrawing graph) :
    ∃ D' : Paper170.AdmissibleDrawing graph,
      (∀ e, HasFiniteAffineCover (D'.edge e)) ∧ Paper170.crossingCount D' ≤ finiteCrossingCount D := by
…

    Mentions: OAI.Paper170Geometry.FiniteIntersectionDrawing, OAI.Paper170Geometry.finiteCrossingCount

  15. theorem OAI.Paper170Geometry.polygonal_normalization line 265

    Source documentation

    An arbitrary admissible continuous drawing admits an actual admissible polygonal drawing with no more spatial crossing points. Vertices and routes are allowed to move. No one-crossing-per-pair or adjacency condition is assumed.

    theorem polygonal_normalization [Fintype Vertex] [Fintype Edge] (D : Paper170.AdmissibleDrawing graph) :
    ∃ D' : Paper170.AdmissibleDrawing graph,
      (∀ e, HasFiniteAffineCover (D'.edge e)) ∧ Paper170.crossingCount D' ≤ Paper170.crossingCount D := by
…
  16. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossingOrigin_eq_innerMark line 291
  17. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_origin_mem_pair line 303
  18. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_origin_surj_of_count_eq line 325
  19. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_pair_retained_of_count_eq line 346
  20. theorem OAI.Paper170Geometry.exists_drawing_subdivision_at line 386
  21. theorem OAI.Paper170Geometry.PolygonalExterior.exists_assembled_port_subdivision line 405