Theorems · Theorem · combinatorics

Graph.edgeSet_copy

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

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

0 results in Mathlib

Foundations

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