Theorems · Definition · combinatorics
SimpleGraph.ConnectedComponent.supp
{V : Type u} → {G : SimpleGraph V} → G.ConnectedComponent → Set VThe set of vertices in a connected component of a graph.
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 5 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.
- Setstatement · cited by 53,352
- Set.ofPredproof · cited by 6,101
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.ConnectedComponentstatement and proof · cited by 86
- SimpleGraph.connectedComponentMkproof · cited by 40
Cited by46
Results whose statement or proof uses this declaration.
- SimpleGraph.ConnectedComponent.toSimpleGraphproof · cited by 14
- SimpleGraph.oddComponentsproof · cited by 10
- SimpleGraph.ConnectedComponent.toSubgraphproof · cited by 5
- SimpleGraph.ConnectedComponent.mem_supp_iffstatement · cited by 4
- SimpleGraph.ConnectedComponent.eq_of_common_vertexstatement and proof · cited by 2
- SimpleGraph.ConnectedComponent.mem_supp_congr_adjstatement · cited by 2
- SimpleGraph.ConnectedComponent.nonempty_suppstatement · cited by 2
- SimpleGraph.ConnectedComponent.reachable_of_mem_suppstatement and proof · cited by 2
- SimpleGraph.ConnectedComponent.supp_injectivestatement · cited by 2
- SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singletonstatement and proof · cited by 2
- SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraphstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.biUnion_supp_eq_suppstatement and proof · cited by 1