Native induced-path interface

The local edge/nonedge predicate is equivalent to exclusion of Mathlib's pathGraph 4 by IsIndContained. This connects the structural classes to native induced graph embeddings without a parallel notion of containment.

theorem SimpleGraph.IsP4Free.not_pathGraph_four_isIndContained {V : Type u_1} {G : SimpleGraph V} (h : G.IsP4Free) : ¬(pathGraph 4).IsIndContained G

The local P₄ exclusion predicate excludes native induced path embeddings.

theorem SimpleGraph.pathGraph_four_isIndContained_of_adj {V : Type u_1} {G : SimpleGraph V} {a b c d : V} (hab : G.Adj a b) (hbc : G.Adj b c) (hcd : G.Adj c d) (hac : ¬G.Adj a c) (had : ¬G.Adj a d) (hbd : ¬G.Adj b d) : (pathGraph 4).IsIndContained G

Four vertices satisfying the path edges and nonedges give a native induced embedding.

theorem SimpleGraph.isP4Free_iff_not_pathGraph_four_isIndContained {V : Type u_1} {G : SimpleGraph V} : G.IsP4Free ↔ ¬(pathGraph 4).IsIndContained G

Local path exclusion and native induced-path exclusion are equivalent, without finiteness.