Theorems · Definition · combinatorics

Graph.IsLink

{α : Type u_3} → {β : Type u_4} → Graph α β → β → α → α → Prop

The binary incidence predicate, stating that x and y are the ends of an edge e. If G.IsLink e x y then we refer to e as edge and x and y as left and right.

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

124 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms