Theorems · Definition · combinatorics

SimpleGraph.Iso.induce

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

The restriction of an isomorphism of graphs to induced subgraphs.

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

3 results in Mathlib

Foundations

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