Theorems · Theorem · combinatorics

Graph.map_isLink

∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) (e : β) (a a_1 : α'),
  (Graph.map f G).IsLink e a a_1 = Relation.Map (G.IsLink e) f f a a_1

Defined in

Mathlib.Combinatorics.Graph.Maps

Cited by

4 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext