Block graphs
Lax560391.BlockGraphs · concepts/Lax560391/BlockGraphs.lean · lax-560391
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A block graph is a graph with no induced cycle of length at least four and no induced diamond (a complete four-vertex graph minus one edge). Equivalently, every block is a clique. Empty and disconnected graphs are allowed.
Concept map
Lean source view on GitHub
| 1 | import Lax560391.ChordalGraphs |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Block graphs |
| 6 | type: definition |
| 7 | --- |
| 8 | A block graph is a graph with no induced cycle of length at least four |
| 9 | and no induced diamond (a complete four-vertex graph minus one edge). |
| 10 | Equivalently, every block is a clique. Empty and disconnected graphs are allowed. |
| 11 | -/ |
| 12 | |
| 13 | namespace Lax560391.BlockGraphs |
| 14 | |
| 15 | open Lax560391.ChordalGraphs |
| 16 | |
| 17 | /-- The four vertices induce a diamond, `K₄` with edge `cd` removed. -/ |
| 18 | def IsInducedDiamond {V : Type} (G : SimpleGraph V) (a b c d : V) : Prop := |
| 19 | ([a, b, c, d] : List V).Nodup ∧ |
| 20 | G.Adj a b ∧ G.Adj a c ∧ G.Adj a d ∧ |
| 21 | G.Adj b c ∧ G.Adj b d ∧ ¬ G.Adj c d |
| 22 | |
| 23 | /-- Block graphs are the chordal, diamond-free graphs. -/ |
| 24 | def IsBlock {V : Type} (G : SimpleGraph V) : Prop := |
| 25 | IsChordal G ∧ ¬ ∃ a b c d : V, IsInducedDiamond G a b c d |
| 26 | |
| 27 | end Lax560391.BlockGraphs |
| 28 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments