definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A Halin graph is obtained from a plane tree with no vertex of degree two by joining its leaves in their cyclic order. The construction contains the chosen crossing-free embedding because the word "plane" is part of the defining data, rather than attaching a separate planarity proposition.
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Acyclic |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 3 | import Lax68.StraightLineDrawings |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Halin graphs |
| 8 | type: definition |
| 9 | --- |
| 10 | A Halin graph is obtained from a plane tree with no vertex of degree two by |
| 11 | joining its leaves in their cyclic order. The construction |
| 12 | contains the chosen crossing-free embedding because the word "plane" is part |
| 13 | of the defining data, rather than attaching a separate planarity proposition. |
| 14 | -/ |
| 15 | |
| 16 | set_option autoImplicit false |
| 17 | |
| 18 | namespace Lax68.HalinGraphs |
| 19 | |
| 20 | def IsLeaf {V : Type*} (T : SimpleGraph V) (v : V) : Prop := |
| 21 | (T.neighborSet v).ncard = 1 |
| 22 | |
| 23 | def CycleAdjacent {n : ℕ} (i j : Fin n) : Prop := |
| 24 | i.val + 1 = j.val ∨ |
| 25 | j.val + 1 = i.val ∨ |
| 26 | (i.val = 0 ∧ j.val + 1 = n) ∨ |
| 27 | (j.val = 0 ∧ i.val + 1 = n) |
| 28 | |
| 29 | def IsCycleOn {V : Type*} |
| 30 | (R : SimpleGraph V) (S : Set V) : Prop := |
| 31 | (∀ ⦃u v⦄, R.Adj u v → u ∈ S ∧ v ∈ S) ∧ |
| 32 | ∃ n : ℕ, |
| 33 | 3 ≤ n ∧ |
| 34 | ∃ e : Fin n ≃ {v : V // v ∈ S}, |
| 35 | ∀ i j, |
| 36 | R.Adj (e i).1 (e j).1 ↔ CycleAdjacent i j |
| 37 | |
| 38 | structure Construction {V : Type*} (G : SimpleGraph V) where |
| 39 | tree : SimpleGraph V |
| 40 | rim : SimpleGraph V |
| 41 | tree_isTree : tree.IsTree |
| 42 | noDegreeTwo : ∀ v, (tree.neighborSet v).ncard ≠ 2 |
| 43 | rimCycle : IsCycleOn rim {v | IsLeaf tree v} |
| 44 | graph_eq : G = tree ⊔ rim |
| 45 | drawing : StraightLineDrawings.StraightLineDrawing G |
| 46 | |
| 47 | def IsHalin {V : Type*} (G : SimpleGraph V) : Prop := |
| 48 | Nonempty (Construction G) |
| 49 | |
| 50 | end Lax68.HalinGraphs |
| 51 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments