Theorems · Definition · combinatorics

Graph.Inc

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

The unary incidence predicate of G. G.Inc e x means that the vertex x is one or both of the ends of the edge e. In the Inc namespace, we use edge and vertex to refer to e and x.

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

42 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms