Theorems · Definition · combinatorics

Graph.IsNonloopAt

{α : Type u_1} → {β : Type u_2} → Graph α β → β → α → Prop

G.IsNonloopAt e x means that the vertex x is one but not both of the ends of the edge =e, or equivalently that e is incident with x but not a loop at x - see Graph.isNonloopAt_iff_inc_not_isLoopAt.

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

16 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms