Theorems · Definition · combinatorics

SimpleGraph.Embedding

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

A graph embedding is an embedding f such that for vertices v w : V, G'.Adj (f v) (f w) ↔ G.Adj v w. Its image is an induced subgraph of G'. The notation G ↪g G' represents the type of graph embeddings.

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

41 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms