Theorems · Definition · combinatorics

SimpleGraph.Iso

{V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Type (max u_1 u_2)

A graph isomorphism is a bijective map on vertex sets that respects adjacency relations. The notation G ≃g G' represents the type of graph isomorphisms.

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

99 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms