English
For a finite vertex type V with |V| = n, the graph G.overFin n is a graph on Fin n obtained by transporting the vertices along a fixed equivalence.
Русский
Для конечного типа вершин V с |V| = n граф G.overFin n является графом на Fin n, полученным перенесением вершин по фиксированной эквиваленции.
LaTeX
$$$$G.overFin\\; n$$ is a graph on $\\mathrm{Fin}(n)$ constructed from $G$ via a fixed card-equal equivalence.$$
Lean4
/-- Given a graph over a finite vertex type `V` and a proof `hc` that `Fintype.card V = n`,
`G.overFin n` is an isomorphic (as shown in `overFinIso`) graph over `Fin n`. -/
def overFin (hc : Fintype.card V = n) : SimpleGraph (Fin n)
where
Adj x y := G.Adj ((Fintype.equivFinOfCardEq hc).symm x) ((Fintype.equivFinOfCardEq hc).symm y)
symm x y := by simp_rw [adj_comm, imp_self]
