Theorems · Definition · combinatorics

SimpleGraph.Copy.isoSubgraphMap

{α : Type u_4} →
  {β : Type u_5} →
    {A : SimpleGraph α} →
      {B : SimpleGraph β} → (f : A.Copy B) → (A' : A.Subgraph) → A'.coe ≃g (SimpleGraph.Subgraph.map f.toHom A').coe

The isomorphism from a subgraph of A to its map under a copy f : Copy A B.

Defined in

Mathlib.Combinatorics.SimpleGraph.Copy

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound