Theorems · Definition · combinatorics

Quiver.Costar

{U : Type u_1} → [Quiver U] → U → Type (max u_1 u)

The Quiver.Costar at a vertex is the collection of arrows whose target is the vertex. The type Quiver.Costar v is defined to be Σ (u : U), (u ⟶ v).

Defined in

Mathlib.Combinatorics.Quiver.Covering

Cited by

19 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Quiver