Theorems · Definition · combinatorics
SimpleGraph.ConnectedComponent.Represents
{V : Type u} → {G : SimpleGraph V} → Set V → Set G.ConnectedComponent → PropA set of vertices represents a set of components if it contains exactly one vertex from each component.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 8 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 and proof · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- Set.BijOnproof · cited by 168
- SimpleGraph.ConnectedComponentstatement and proof · cited by 86
- SimpleGraph.connectedComponentMkproof · cited by 40
Cited by10
Results whose statement or proof uses this declaration.
- SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singletonstatement and proof · cited by 2
- SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_memstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMemstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.even_ncard_supp_sdiff_repstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMemstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.Represents.existsUnique_repstatement and proof · cited by 1
- SimpleGraph.ConnectedComponent.Represents.ncard_interstatement and proof · cited by 0
- SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_unionstatement and proof · cited by 0
- SimpleGraph.ConnectedComponent.Represents.image_outstatement · cited by 0
- SimpleGraph.ConnectedComponent.Represents.ncard_eqstatement and proof · cited by 0