Theorems · Definition · combinatorics

SimpleGraph.Subgraph.restrict

{V : Type u} → {G : SimpleGraph V} → {G' : G.Subgraph} → G.Subgraph → G'.coe.Subgraph

Given a subgraph of G, restrict it to being a subgraph of another subgraph G' by taking the portion of G that intersects G'.

Defined in

Mathlib.Combinatorics.SimpleGraph.Subgraph

Cited by

3 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms