M-Witness and M-Graph
Lax630294.MGraph · concepts/Lax630294/MGraph.lean · lax-630294
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An -witness of a multigraph consists of pairwise edge-disjoint subgraphs , , of , where is a cycle of length at least four and each is a spanning forest of with exactly four components, each of which contains a vertex of . A multigraph admits an -witness if it has one, and it is an -graph if it admits an -witness and is not a -graph.
Concept map
In the paper
- page 4 of this submission's paper
Lean source view on GitHub
| 1 | import Lax630294.TGraph |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: M-Witness and M-Graph |
| 6 | type: definition |
| 7 | --- |
| 8 | |
| 9 | An *`M`-witness* of a multigraph `G` consists of pairwise edge-disjoint subgraphs |
| 10 | `C`, `F₁`, `F₂` of `G`, where `C` is a cycle of length at least four and each `Fᵢ` |
| 11 | is a spanning forest of `G` with exactly four components, each of which contains |
| 12 | a vertex of `C`. A multigraph *admits an `M`-witness* if it has one, and it is an |
| 13 | *`M`-graph* if it admits an `M`-witness and is not a `T`-graph. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | Subgraphs are given by their edge sets, as in the concept of spanning forests. |
| 18 | The requirement that each component of `Fᵢ` contains a vertex of `C` is stated as: |
| 19 | every vertex of `G` is connected in `Fᵢ` to a vertex incident to an edge of `C`. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax630294.MGraph |
| 23 | |
| 24 | open Graph Lax630294.SpanningStructures Lax630294.TGraph |
| 25 | |
| 26 | variable {α β : Type*} |
| 27 | |
| 28 | /-- `F` is a spanning forest of `G` with four components, each containing a vertex |
| 29 | of the cycle `C`. -/ |
| 30 | def IsFourComponentForestMeeting (G : Graph α β) (C F : Set β) : Prop := |
| 31 | IsSpanningForest G F 4 ∧ |
| 32 | ∀ x : V(G), ∃ c : V(G), (c : α) ∈ incidentVertices G C ∧ (underlying G F).Reachable x c |
| 33 | |
| 34 | /-- `C, F₁, F₂` is an `M`-witness of `G`. -/ |
| 35 | def IsMWitness (G : Graph α β) (C F₁ F₂ : Set β) : Prop := |
| 36 | IsCycle G C ∧ 4 ≤ C.encard ∧ |
| 37 | IsFourComponentForestMeeting G C F₁ ∧ IsFourComponentForestMeeting G C F₂ ∧ |
| 38 | Disjoint C F₁ ∧ Disjoint C F₂ ∧ Disjoint F₁ F₂ |
| 39 | |
| 40 | /-- `G` admits an `M`-witness. -/ |
| 41 | def AdmitsMWitness (G : Graph α β) : Prop := |
| 42 | ∃ C F₁ F₂ : Set β, IsMWitness G C F₁ F₂ |
| 43 | |
| 44 | /-- `G` is an `M`-graph: it admits an `M`-witness and is not a `T`-graph. -/ |
| 45 | def IsMGraph (G : Graph α β) : Prop := |
| 46 | AdmitsMWitness G ∧ ¬ IsTGraph G |
| 47 | |
| 48 | end Lax630294.MGraph |
| 49 |
Formalization notes
Subgraphs are given by their edge sets, as in the concept of spanning forests. The requirement that each component of contains a vertex of is stated as: every vertex of is connected in to a vertex incident to an edge of .
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments