Theorems · Inductive type · combinatorics

Prefunctor.IsCovering

{U : Type u_1} → [inst : Quiver U] → {V : Type u_2} → [inst_1 : Quiver V] → U ⥤q V → Prop

A prefunctor is a covering of quivers if it defines bijections on all stars and costars.

Defined in

Mathlib.Combinatorics.Quiver.Covering

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

QuiverQuiver