Theorems · Definition · combinatorics
Graph.Compatible
{α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → PropTwo graphs are compatible if their shared edges have the same ends in both graphs.
- Defined in
- Mathlib.Combinatorics.Graph.Basic
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Graphstatement and proof · cited by 242
- Graph.IsLinkproof · cited by 124
- Graph.edgeSetproof · cited by 79
Cited by21
Results whose statement or proof uses this declaration.
- Graph.Compatible.extstatement and proof · cited by 9
- Graph.Compatible.of_le_lestatement · cited by 9
- Graph.IsSubgraph.compatiblestatement · cited by 3
- Graph.Compatible.le_iffstatement and proof · cited by 3
- Graph.Compatible.of_lestatement · cited by 3
- Graph.IsLink.of_compatiblestatement and proof · cited by 3
- Graph.Inc.of_compatiblestatement and proof · cited by 2
- Graph.IsSubgraph.compatible'statement · cited by 2
- Graph.Compatible.symmstatement and proof · cited by 2
- Graph.Compatible.anti_leftstatement and proof · cited by 2
- Graph.le_iff_compatible_subset_subsetstatement and proof · cited by 1
- Graph.Compatible.anti_rightstatement and proof · cited by 1