Exclusion of induced four-vertex paths

The three edges and three nonedges below force all four vertices to be distinct. No finiteness hypothesis is needed for this local exclusion predicate.

def SimpleGraph.IsP4Free {V : Type u_1} (G : SimpleGraph V) : Prop

There is no induced path on four vertices, in the order a, b, c, d.

Equations

• G.IsP4Free = ∀ (a b c d : V), G.Adj a b → G.Adj b c → G.Adj c d → ¬G.Adj a c → ¬G.Adj a d → ¬G.Adj b d → False

theorem SimpleGraph.IsP4Free.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (h : G.IsP4Free) (f : W → V) : (SimpleGraph.comap f G).IsP4Free

Four-vertex path exclusion pulls back along vertex maps.

theorem SimpleGraph.IsP4Free.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsP4Free) (s : Set V) : (SimpleGraph.induce s G).IsP4Free

Every induced subgraph of a graph excluding P₄ also excludes P₄.

theorem SimpleGraph.Iso.isP4Free_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : G.IsP4Free ↔ H.IsP4Free

Graph isomorphisms preserve induced four-vertex path exclusion.

theorem SimpleGraph.IsP4Free.compl {V : Type u_1} {G : SimpleGraph V} (h : G.IsP4Free) : Gᶜ.IsP4Free

The complement of an induced P₄ is another induced P₄.

@[simp]

theorem SimpleGraph.isP4Free_compl {V : Type u_1} {G : SimpleGraph V} : Gᶜ.IsP4Free ↔ G.IsP4Free

Four-vertex path exclusion is invariant under complementation.