Theorems · Theorem · combinatorics

Graph.Compatible.isLink_congr

∀ {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β},
  e ∈ G.edgeSet → e ∈ H.edgeSet → G.Compatible H → ∀ {x y : α}, G.IsLink e x y ↔ H.IsLink e x y

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

1 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms