definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A finite wheel consists of a cycle of at least three rim vertices together with one hub adjacent to every rim vertex, and has no other edges.
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.UniversalVerts |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Wheels |
| 6 | type: definition |
| 7 | --- |
| 8 | A finite wheel consists of a cycle of at least three rim vertices together |
| 9 | with one hub adjacent to every rim vertex, and has no other edges. |
| 10 | -/ |
| 11 | |
| 12 | set_option autoImplicit false |
| 13 | |
| 14 | namespace Lax68.Wheels |
| 15 | |
| 16 | def CycleAdjacent {n : ℕ} (i j : Fin n) : Prop := |
| 17 | i.val + 1 = j.val ∨ |
| 18 | j.val + 1 = i.val ∨ |
| 19 | (i.val = 0 ∧ j.val + 1 = n) ∨ |
| 20 | (j.val = 0 ∧ i.val + 1 = n) |
| 21 | |
| 22 | def IsCycleOn {V : Type*} |
| 23 | (R : SimpleGraph V) (S : Set V) : Prop := |
| 24 | (∀ ⦃u v⦄, R.Adj u v → u ∈ S ∧ v ∈ S) ∧ |
| 25 | ∃ n : ℕ, |
| 26 | 3 ≤ n ∧ |
| 27 | ∃ e : Fin n ≃ {v : V // v ∈ S}, |
| 28 | ∀ i j, |
| 29 | R.Adj (e i).1 (e j).1 ↔ CycleAdjacent i j |
| 30 | |
| 31 | def HasWheelShape {V : Type*} (G : SimpleGraph V) : Prop := |
| 32 | ∃ hub : V, |
| 33 | hub ∈ G.universalVerts ∧ |
| 34 | ∃ rim : SimpleGraph V, |
| 35 | IsCycleOn rim {v | v ≠ hub} ∧ |
| 36 | ∀ ⦃u v⦄, |
| 37 | u ≠ hub → |
| 38 | v ≠ hub → |
| 39 | (G.Adj u v ↔ rim.Adj u v) |
| 40 | |
| 41 | def IsWheel {V : Type*} (G : SimpleGraph V) : Prop := |
| 42 | HasWheelShape G |
| 43 | |
| 44 | end Lax68.Wheels |
| 45 |
Builds on
none
From Mathlib
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