Theorems · Definition · combinatorics
SimpleGraph.replaceVertex
{V : Type u_1} → SimpleGraph V → V → V → [DecidableEq V] → SimpleGraph VThe graph formed by forgetting t's neighbours and instead giving it those of s. The s-t
edge is removed if present.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjproof · cited by 1,346
Cited by15
Results whose statement or proof uses this declaration.
- SimpleGraph.CliqueFree.replaceVertexstatement and proof · cited by 3
- SimpleGraph.adj_replaceVertex_iff_of_nestatement · cited by 2
- SimpleGraph.card_edgeFinset_replaceVertex_of_not_adjstatement · cited by 2
- SimpleGraph.IsTuranMaximal.isEquipartitionproof · cited by 1
- SimpleGraph.IsTuranMaximal.not_adj_transproof · cited by 1
- SimpleGraph.edgeSet_replaceVertex_of_adjstatement · cited by 1
- SimpleGraph.card_edgeFinset_replaceVertex_of_adjstatement · cited by 1
- SimpleGraph.edgeSet_replaceVertex_of_not_adjstatement · cited by 1
- SimpleGraph.IsTuranMaximal.degree_eq_of_not_adjproof · cited by 1
- SimpleGraph.replaceVertex_selfstatement · cited by 1
- SimpleGraph.edgeFinset_replaceVertex_of_adjstatement and proof · cited by 1
- SimpleGraph.edgeFinset_replaceVertex_of_not_adjstatement and proof · cited by 1