fix(combinatorics/simple_graph/connectivity): correctly generalized v…

…ariables (#13405)
leanprover-community · Apr 13, 2022 · b0bd771 · b0bd771
1 parent 917fc96
commit b0bd771
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/combinatorics/simple_graph/connectivity.lean b/src/combinatorics/simple_graph/connectivity.lean
@@ -57,10 +57,10 @@ walks, trails, paths, circuits, cycles
 
 -/
 
-universes u
+universes u v
 
 namespace simple_graph
-variables {V V' : Type u} (G G' : simple_graph V)
+variables {V : Type u} {V' : Type v} (G : simple_graph V) (G' : simple_graph V')
 
 /-- A walk is a sequence of adjacent vertices.  For vertices `u v : V`,
 the type `walk u v` consists of all walks starting at `u` and ending at `v`.