Theorems · Definition · combinatorics

SimpleGraph.overFin

{V : Type u_1} → SimpleGraph V → [inst : Fintype V] → {n : ℕ} → Fintype.card V = n → SimpleGraph (Fin n)

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.

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype