Induced digraphs

The digraph D.induce S induced by a digraph D on a set S of its vertices has the vertices of S, two of which are adjacent exactly when they are adjacent in D. Inducing on the complement of a set of vertices deletes those vertices.

Main definitions

• Digraph.induce: the digraph D.induce S induced by D on a set S of vertices.

def Digraph.induce {V : Type u} (D : Digraph V) (S : Set V) : Digraph ↑S

The digraph induced by D on a set S of vertices: two vertices of S are adjacent when they are adjacent in D.

@[simp]

theorem Digraph.induce_adj {V : Type u} {D : Digraph V} {S : Set V} {v w : ↑S} : (D.induce S).Adj v w ↔ D.Adj ↑v ↑w