OAI/Combinatorics/PlanarL1/PlanarMetric.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Topology.Drawing.Split.param line 14
  2. lemma OAI.PlanarL1.Topology.Drawing.Split.param_injective line 17
  3. lemma OAI.PlanarL1.Topology.Drawing.Split.param_interior line 26
  4. def OAI.PlanarL1.Topology.Drawing.Split.piecePath line 33
  5. lemma OAI.PlanarL1.Topology.Drawing.Split.piecePath_apply line 37
  6. lemma OAI.PlanarL1.Topology.Drawing.Split.piecePath_injective line 40
  7. abbrev OAI.PlanarL1.Topology.Drawing.Split.Directed line 43
  8. def OAI.PlanarL1.Topology.Drawing.Split.start line 45
  9. def OAI.PlanarL1.Topology.Drawing.Split.finish line 47
  10. def OAI.PlanarL1.Topology.Drawing.Split.flip line 49
  11. lemma OAI.PlanarL1.Topology.Drawing.Split.start_flip line 51
  12. lemma OAI.PlanarL1.Topology.Drawing.Split.finish_flip line 54
  13. lemma OAI.PlanarL1.Topology.Drawing.Split.start_ne_finish line 57
  14. def OAI.PlanarL1.Topology.Drawing.Split.arc line 62
  15. lemma OAI.PlanarL1.Topology.Drawing.Split.arc_injective line 66
  16. lemma OAI.PlanarL1.Topology.Drawing.Split.arc_location line 76
  17. def OAI.PlanarL1.Topology.Drawing.Split.graph line 86
  18. lemma OAI.PlanarL1.Topology.Drawing.Split.unsplit_adj line 95
  19. lemma OAI.PlanarL1.Topology.Drawing.Split.first_adj line 99
  20. lemma OAI.PlanarL1.Topology.Drawing.Split.last_adj line 102
  21. lemma OAI.PlanarL1.Topology.Drawing.Split.middle_adj line 105
  22. def OAI.PlanarL1.Topology.Drawing.Split.drawing line 108
  23. def OAI.PlanarL1.Topology.Drawing.pullback line 146
  24. def OAI.PlanarL1.Weighted.EnlargedTree.splitSet line 167
  25. def OAI.PlanarL1.Weighted.EnlargedTree.splitTip line 170
  26. lemma OAI.PlanarL1.Weighted.EnlargedTree.splitTip_injective line 175
  27. def OAI.PlanarL1.Weighted.EnlargedTree.splitMap line 188
  28. lemma OAI.PlanarL1.Weighted.EnlargedTree.splitMap_injective line 192
  29. def OAI.PlanarL1.Weighted.EnlargedTree.drawingGraph line 202
  30. lemma OAI.PlanarL1.Weighted.EnlargedTree.original_tree_adj line 205
  31. lemma OAI.PlanarL1.Weighted.EnlargedTree.branch_adj line 214
  32. lemma OAI.PlanarL1.Weighted.EnlargedTree.tree_le_drawingGraph line 224
  33. lemma OAI.PlanarL1.Weighted.EnlargedTree.pair_adj line 237
  34. def OAI.PlanarL1.Weighted.EnlargedTree.enlargedDrawing line 253
  35. lemma OAI.PlanarL1.Weighted.EnlargedTree.reverse_ne line 269
  36. def OAI.PlanarL1.Weighted.EnlargedTree.matchingGraph line 274
  37. lemma OAI.PlanarL1.Weighted.EnlargedTree.matchingGraph_height line 284
  38. lemma OAI.PlanarL1.Weighted.EnlargedTree.matchingGraph_matching line 291
  39. lemma OAI.PlanarL1.Weighted.EnlargedTree.layout_of_planar line 299
  40. def OAI.PlanarL1.HeightTree.rootLeafLayout line 319
  41. lemma OAI.PlanarL1.Weighted.EnlargedTree.exact_layout_of_planar line 345

    Source documentation

    The source's exact topology-to-column-layout bridge, including a singleton incidence tree. The contour and the noncrossing switches are constructed, not assumed.

    lemma exact_layout_of_planar (hp : IsPlanar G) :
    ∃ n : ℕ, ∃ L : (tree hc hs hl o).Layout n, ExactPairs L := by
…

    Mentions: OAI.PlanarL1.IsPlanar, OAI.PlanarL1.Weighted.EnlargedTree.tree, OAI.PlanarL1.Weighted.EnlargedTree.ExactPairs

  42. lemma OAI.PlanarL1.Weighted.EnlargedTree.column_model_of_planar line 361

    Source documentation

    Every literal planar weighted graph is isometric on its original vertices to the constructed terminal noncrossing column model.

    lemma column_model_of_planar (hp : IsPlanar G) :
    ∃ n : ℕ, ∃ L : (tree hc hs hl o).Layout n, ExactPairs L ∧
      ∀ u v : V, (L.point (.inl u)).distance (L.point (.inl v))=graphDistance G l u v := by
…

    Mentions: OAI.PlanarL1.IsPlanar, OAI.PlanarL1.Weighted.EnlargedTree.tree, OAI.PlanarL1.Weighted.EnlargedTree.ExactPairs, OAI.PlanarL1.graphDistance