OAI/Combinatorics/PlanarL1/Layout.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.HeightTree.growth_exists line 15
  2. def OAI.PlanarL1.HeightTree.internal line 46
  3. lemma OAI.PlanarL1.HeightTree.mem_internal line 49
  4. lemma OAI.PlanarL1.HeightTree.internal_closed line 51
  5. lemma OAI.PlanarL1.HeightTree.internal_scope line 59
  6. lemma OAI.PlanarL1.HeightTree.internal_frontier line 67
  7. lemma OAI.PlanarL1.HeightTree.tree_core line 81

    Source documentation

    Every actual polygonally drawn finite tree can be enclosed in a convex disk, with the leaf stubs left as disjoint exterior polygonal arcs. All untouched raw leaf-to-leaf drawing pieces remain outside the closed disk.

    lemma tree_core (hG : T.graph ≤ G) (hroot : ¬T.IsLeaf T.root) :
    ∃ C : DiskCore T.graph {v | T.IsLeaf v},
      ∃ E : ExteriorPorts C.drawing.point P.point {v | T.IsLeaf v} C.disk,
        Disjoint (closure C.disk) (P.carrier {v | T.IsLeaf v}) ∧
        ∀ v, T.IsLeaf v → ∀ z∈E.region v, z∈P.carrier {v | T.IsLeaf v} → z=P.point v := by
…
  8. lemma OAI.PlanarL1.Topology.PolygonallyJoined.exists_path line 115
  9. lemma OAI.PlanarL1.Topology.DiskCore.carrier_subset line 127
  10. lemma OAI.PlanarL1.HeightTree.ancestor_plpath line 144
  11. lemma OAI.PlanarL1.HeightTree.descendants_pljoined line 157
  12. lemma OAI.PlanarL1.HeightTree.nondescendants_pljoined line 164
  13. lemma OAI.PlanarL1.HeightTree.core_prefix_connected line 173
  14. lemma OAI.PlanarL1.HeightTree.layout_of_core line 204
  15. def OAI.PlanarL1.Topology.stemCarrier line 273

    Source documentation

    The untouched raw carrier together with the actual exterior stubs.

    def stemCarrier (S : Set V) : Set ℂ := P.carrier S ∪ ⋃ v : S, E.region v.val
  16. lemma OAI.PlanarL1.Topology.stemCarrier_disjoint line 275
  17. lemma OAI.PlanarL1.HeightTree.layout_of_drawing line 306

    Source documentation

    The literal planar leaf layout is constructed from a real raw drawing of its tree and terminal matching. Neither a contour order nor a disk is assumed.

    lemma layout_of_drawing (P : PLDrawing G) (hG : T.graph ≤ G) (hroot : ¬T.IsLeaf T.root)
    (M : SimpleGraph {v : V // T.IsLeaf v})
    (hMG : ∀ i j, M.Adj i j → G.Adj i.val j.val)
    (hheight : ∀ i j, M.Adj i j → T.height i.val=T.height j.val)
    (hmatch : ∀ i j k, M.Adj i j → M.Adj i k → j=k) :
    ∃ (L : T.Layout (Fintype.card {v : V // T.IsLeaf v})),
      ∀ i j, L.pair.Adj i j ↔ M.Adj ⟨L.leaf i,L.isLeaf i⟩ ⟨L.leaf j,L.isLeaf j⟩ := by
…
  18. lemma OAI.PlanarL1.Topology.Drawing.forward_interior_meet line 367
  19. abbrev OAI.PlanarL1.Topology.Drawing.Split.Tip line 379
  20. abbrev OAI.PlanarL1.Topology.Drawing.Split.Node line 380
  21. abbrev OAI.PlanarL1.Topology.Drawing.Split.Piece line 381
  22. def OAI.PlanarL1.Topology.Drawing.Split.tipTime line 383
  23. lemma OAI.PlanarL1.Topology.Drawing.Split.tipTime_pos line 389
  24. lemma OAI.PlanarL1.Topology.Drawing.Split.tipTime_lt_one line 390
  25. def OAI.PlanarL1.Topology.Drawing.Split.point line 394
  26. lemma OAI.PlanarL1.Topology.Drawing.Split.point_injective line 398
  27. def OAI.PlanarL1.Topology.Drawing.Split.meshNode line 416
  28. def OAI.PlanarL1.Topology.Drawing.Split.meshTime line 421
  29. lemma OAI.PlanarL1.Topology.Drawing.Split.mesh_point line 429
  30. def OAI.PlanarL1.Topology.Drawing.Split.label line 433
  31. def OAI.PlanarL1.Topology.Drawing.Split.src line 437
  32. def OAI.PlanarL1.Topology.Drawing.Split.dst line 441
  33. def OAI.PlanarL1.Topology.Drawing.Split.first line 445
  34. def OAI.PlanarL1.Topology.Drawing.Split.last line 449
  35. lemma OAI.PlanarL1.Topology.Drawing.Split.first_lt_last line 453
  36. lemma OAI.PlanarL1.Topology.Drawing.Split.src_point line 458
  37. lemma OAI.PlanarL1.Topology.Drawing.Split.dst_point line 464
  38. lemma OAI.PlanarL1.Topology.Drawing.Split.src_ne_dst line 470
  39. lemma OAI.PlanarL1.Topology.Drawing.Split.interior_point_avoid line 477
  40. lemma OAI.PlanarL1.Topology.Drawing.Split.interior_piece_unique line 501