Theorems · Definition · combinatorics

Graph.deleteEdges

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

Delete a set F of edges from G. This is a special case of restrict, but we define it with copy so that the edge set is definitionally equal to E(G) \ F.

Defined in

Mathlib.Combinatorics.Graph.Delete

Cited by

12 results in Mathlib

Foundations

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