Theorems · Definition · combinatorics
SimpleGraph.Subgraph.deleteEdges
{V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set (Sym2 V) → G.SubgraphGiven a subgraph G' and a set of vertex pairs, remove all of the corresponding edges
from its edge set, if present.
See also: SimpleGraph.deleteEdges.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- Sym2statement and proof · cited by 737
- SimpleGraph.Subgraphstatement and proof · cited by 326
- SimpleGraph.Subgraph.vertsproof · cited by 210
- SimpleGraph.Subgraph.Adjproof · cited by 147
- Sym2.ToRelproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- SimpleGraph.Subgraph.deleteEdges_lestatement · cited by 1
- SimpleGraph.Subgraph.spanningCoe_deleteEdges_lestatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_adjstatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_coe_eqstatement and proof · cited by 0
- SimpleGraph.Subgraph.deleteEdges_deleteEdgesstatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_empty_eqstatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eqstatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eqstatement · cited by 0
- SimpleGraph.Subgraph.coe_deleteEdges_eqstatement and proof · cited by 0
- SimpleGraph.Subgraph.coe_deleteEdges_lestatement and proof · cited by 0
- SimpleGraph.Subgraph.deleteEdges_le_of_lestatement · cited by 0
- SimpleGraph.Subgraph.deleteEdges_spanningCoe_eqstatement and proof · cited by 0