def Hex.SparseGraph.relabel {n : Nat} (G : SparseGraph n) (p : Perm n) : SparseGraph n

Relabel by the bijection from new vertices to old vertices. Neighbours are mapped by its inverse and sorted, without a dense adjacency matrix.

Equations

• G.relabel p = Hex.SparseGraph.ofRows (Vector.ofFn fun (i : Fin n) => Hex.SparseGraph.Builder.mapRow (G.nbrs (p.get i)) p.inv.get) ⋯ ⋯ ⋯

@[simp]

theorem Hex.SparseGraph.adj_relabel {n : Nat} (G : SparseGraph n) (p : Perm n) (i j : Fin n) : (G.relabel p).adj i j = G.adj (p.get i) (p.get j)

theorem Hex.SparseGraph.nbrs_relabel_perm {n : Nat} (G : SparseGraph n) (p : Perm n) (i : Fin n) : ((G.relabel p).nbrs i).toList.Perm (List.map p.inv.get (G.nbrs (p.get i)).toList)

Row normalization changes only the order of the mapped neighbours.

@[simp]

theorem Hex.SparseGraph.degree_relabel {n : Nat} (G : SparseGraph n) (p : Perm n) (i : Fin n) : (G.relabel p).degree i = G.degree (p.get i)

theorem Hex.SparseGraph.neighbors_size_eq {n : Nat} (G : SparseGraph n) : G.neighbors.size = (List.ofFn G.degree).sum

The packed storage length is the sum of the row lengths.

@[simp]

theorem Hex.SparseGraph.neighbors_size_relabel {n : Nat} (G : SparseGraph n) (p : Perm n) : (G.relabel p).neighbors.size = G.neighbors.size

Relabelling preserves the allocation needed for packed adjacency.

@[simp]

theorem Hex.SparseGraph.relabel_id {n : Nat} (G : SparseGraph n) : G.relabel (Perm.id n) = G

theorem Hex.SparseGraph.relabel_relabel {n : Nat} (G : SparseGraph n) (p q : Perm n) : (G.relabel p).relabel q = G.relabel (p.comp q)

@[simp]

theorem Hex.SparseGraph.toDense_relabel {n : Nat} (G : SparseGraph n) (p : Perm n) : (G.relabel p).toDense = G.toDense.relabel p.get