Theorems · Definition · combinatorics

Graph.induce

{α : Type u_1} → {β : Type u_2} → Graph α β → Set α → Graph α β

The subgraph of G induced by a set X of vertices. The edges are the edges of G with both ends in X. (X is not required to be a subset of V(G) for this definition to work, even though this is the standard use case)

Defined in

Mathlib.Combinatorics.Graph.Delete

Cited by

8 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound