Theorems · Theorem · combinatorics

Graph.map_isLoopAt

∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {e : β} {x : α'} (f : α → α'),
  (Graph.map f G).IsLoopAt e x ↔ ∃ u v, G.IsLink e u v ∧ f u = x ∧ f v = x

Defined in

Mathlib.Combinatorics.Graph.Maps

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext