Theorems · Definition · combinatorics

SimpleGraph.induceHom

{V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {G' : SimpleGraph W} →
        {s : Set V} →
          {t : Set W} → (φ : G →g G') → Set.MapsTo (⇑φ) s t → SimpleGraph.induce s G →g SimpleGraph.induce t G'

The restriction of a morphism of graphs to induced subgraphs.

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

7 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound