Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-28 10:11 188a411e

View on Github →

feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (#17828)

Estimated changes

Created src/combinatorics/quiver/covering.lean

added theorem prefunctor.bijective_costar_iff_bijective_star

added def prefunctor.costar

added theorem prefunctor.costar_apply

added theorem prefunctor.costar_comp

added theorem prefunctor.costar_conj_star

added theorem prefunctor.is_covering.comp

added theorem prefunctor.is_covering.map_injective

added theorem prefunctor.is_covering.of_comp_left

added theorem prefunctor.is_covering.of_comp_right

added theorem prefunctor.is_covering_of_bijective_costar

added theorem prefunctor.is_covering_of_bijective_star

added def prefunctor.path_star

added theorem prefunctor.path_star_apply

added theorem prefunctor.path_star_bijective

added theorem prefunctor.path_star_injective

added theorem prefunctor.path_star_surjective

added def prefunctor.star

added theorem prefunctor.star_apply

added theorem prefunctor.star_comp

added theorem prefunctor.symmetrify_star

added def quiver.costar

added def quiver.path_star

added def quiver.star

added def quiver.star_equiv_costar

added theorem quiver.star_equiv_costar_apply

added theorem quiver.star_equiv_costar_symm_apply

added def quiver.symmetrify_costar

added def quiver.symmetrify_star