Theorems · Definition · combinatorics
SimpleGraph.deleteUniversalVerts
{V : Type u_1} → (G : SimpleGraph V) → G.SubgraphThe subgraph of G with the universal vertices removed.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Subgraphstatement · cited by 326
- SimpleGraph.Subgraph.deleteVertsproof · cited by 15
- SimpleGraph.universalVertsproof · cited by 8
Cited by6
Results whose statement or proof uses this declaration.
- SimpleGraph.disjoint_image_val_universalVertsstatement and proof · cited by 1
- SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_suppstatement and proof · cited by 1
- SimpleGraph.deleteUniversalVerts_vertsstatement and proof · cited by 1
- SimpleGraph.exists_isTutteViolatorproof · cited by 1
- SimpleGraph.deleteUniversalVerts_adjstatement · cited by 0
- SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_unionstatement and proof · cited by 0