Induced minors
Lax762056.InducedMinors · concepts/Lax762056/InducedMinors.lean · lax-762056
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A graph is an induced minor of if its vertices have pairwise disjoint, nonempty connected branch sets in , and two distinct branch sets are joined by an edge exactly when their vertices are adjacent in . Thus edges between retained branch sets cannot be deleted. For finite graphs this is the usual definition by vertex deletions and edge contractions.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Induced minors |
| 6 | type: definition |
| 7 | --- |
| 8 | A graph is an induced minor of if its vertices have pairwise disjoint, |
| 9 | nonempty connected branch sets in , and two distinct branch sets are joined |
| 10 | by an edge exactly when their vertices are adjacent in . Thus edges between |
| 11 | retained branch sets cannot be deleted. For finite graphs this is the usual |
| 12 | definition by vertex deletions and edge contractions. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax762056.InducedMinors |
| 16 | |
| 17 | open SimpleGraph |
| 18 | |
| 19 | structure Model {W V : Type*} (H : SimpleGraph W) (G : SimpleGraph V) where |
| 20 | branch : W → Set V |
| 21 | connected : ∀ v, Connected (G.induce (branch v)) |
| 22 | disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v) |
| 23 | adjacent : ∀ u v, u ≠ v → |
| 24 | (H.Adj u v ↔ ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y) |
| 25 | |
| 26 | def IsInducedMinor {W V : Type*} (H : SimpleGraph W) |
| 27 | (G : SimpleGraph V) : Prop := |
| 28 | Nonempty (Model H G) |
| 29 | |
| 30 | end Lax762056.InducedMinors |
| 31 |
Builds on
none
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments