Prove edge-clique law

algebraic-graphs · Apr 17, 2017 · e59826c · e59826c
1 parent 1b0651a
commit e59826c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/API/Theorems.agda b/src/API/Theorems.agda
@@ -10,6 +10,10 @@ open import Reasoning
 vertices-vertex : ∀ {A} {x : A} -> vertices [ x ] ≡ vertex x
 vertices-vertex = +identity >> reflexivity
 
+-- edge x y == clique [x, y]
+edge-clique : ∀ {A} {x y : A} -> edge x y ≡ clique (x :: [ y ])
+edge-clique = symmetry (R *right-identity)
+
 -- vertices xs ⊆ clique xs
 vertices-clique : ∀ {A} {xs : List A} -> vertices xs ⊆ clique xs
 vertices-clique {_} {[]}     = ⊆reflexivity