Theorems · Definition · combinatorics

Graph.map

{α : Type u_1} → {α' : Type u_2} → {β : Type u_4} → (α → α') → Graph α β → Graph α' β

Map G : Graph α β to a Graph α' β with the same edge set by applying a function f : α → α' to each vertex. Edges between identified vertices become loops.

Defined in

Mathlib.Combinatorics.Graph.Maps

Cited by

16 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext