Theorems · Definition · combinatorics

Graph.copy

{α : Type u_1} →
  {β : Type u_2} →
    (G : Graph α β) →
      {vertexSet : Set α} →
        {edgeSet : Set β} →
          {IsLink : β → α → α → Prop} →
            G.vertexSet = vertexSet →
              G.edgeSet = edgeSet → (∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) → Graph α β

Graph.copy produces a graph equal to G but with provided definitional choices for vertexSet, edgeSet, and IsLink. This is mainly useful for improving definitional equalities while keeping the same underlying graph.

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

4 results in Mathlib

Foundations

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