Documentation Verification Report

Covering

📁 Source: Mathlib/Combinatorics/Quiver/Covering.lean

Statistics

Metric	Count
Definitions `IsCovering`, `costar`, `pathStar`, `Costar`, `mk`, `PathStar`, `mk`, `mk`, `starEquivCostar`, `symmetrifyCostar`, `symmetrifyStar`	11
Theorems `comp`, `costar_bijective`, `map_injective`, `of_comp_left`, `of_comp_right`, `pathStar_bijective`, `star_bijective`, `symmetrify`, `bijective_costar_iff_bijective_star`, `costar_apply`, `costar_comp`, `costar_conj_star`, `costar_fst`, `costar_snd`, `isCovering_of_bijective_costar`, `isCovering_of_bijective_star`, `pathStar_apply`, `pathStar_bijective`, `pathStar_injective`, `pathStar_surjective`, `star_apply`, `star_comp`, `star_fst`, `star_snd`, `symmetrifyCostar`, `symmetrifyStar`, `starEquivCostar_apply`, `starEquivCostar_apply_fst`, `starEquivCostar_apply_snd`, `starEquivCostar_symm_apply`, `starEquivCostar_symm_apply_fst`, `starEquivCostar_symm_apply_snd`	32
Total	43

Prefunctor

Definitions

Name	Category	Theorems
`IsCovering` 📖	CompData	2 math math: `isCovering_of_bijective_costar`, `isCovering_of_bijective_star`
`costar` 📖	CompOp	9 math math: `costar_comp`, `costar_conj_star`, `costar_fst`, `IsCovering.costar_bijective`, `costar_apply`, `symmetrifyStar`, `symmetrifyCostar`, `costar_snd`, `bijective_costar_iff_bijective_star`
`pathStar` 📖	CompOp	5 math math: `pathStar_surjective`, `pathStar_injective`, `pathStar_apply`, `IsCovering.pathStar_bijective`, `pathStar_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_costar_iff_bijective_star` 📖	mathematical	—	`Function.Bijective` `Quiver.Costar` `obj` `costar` `Quiver.Star` `star`	—	`costar_conj_star` `EquivLike.comp_bijective` `EquivLike.bijective_comp`
`costar_apply` 📖	mathematical	—	`costar` `obj` `map`	—	—
`costar_comp` 📖	mathematical	—	`costar` `comp` `Quiver.Costar` `obj`	—	—
`costar_conj_star` 📖	mathematical	—	`costar` `Quiver.Costar` `Quiver.Star` `obj` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Quiver.starEquivCostar` `star` `Equiv.symm`	—	`map_reverse` `Quiver.reverse_reverse`
`costar_fst` 📖	mathematical	—	`Quiver.Hom` `obj` `costar`	—	—
`costar_snd` 📖	mathematical	—	`Quiver.Hom` `obj` `costar` `map`	—	—
`isCovering_of_bijective_costar` 📖	mathematical	`Function.Bijective` `Quiver.Costar` `obj` `costar`	`IsCovering`	—	`bijective_costar_iff_bijective_star`
`isCovering_of_bijective_star` 📖	mathematical	`Function.Bijective` `Quiver.Star` `obj` `star`	`IsCovering`	—	`bijective_costar_iff_bijective_star`
`pathStar_apply` 📖	mathematical	—	`pathStar` `obj` `mapPath`	—	—
`pathStar_bijective` 📖	mathematical	`Function.Bijective` `Quiver.Star` `obj` `star`	`Quiver.PathStar` `pathStar`	—	`pathStar_injective` `pathStar_surjective`
`pathStar_injective` 📖	mathematical	`Quiver.Star` `obj` `star`	`Quiver.PathStar` `pathStar`	—	`Quiver.Path.nil_ne_cons` `Quiver.Path.cast_cons` `Quiver.Path.eq_cast_iff_heq` `Quiver.Path.cons_ne_nil` `Quiver.Path.cast_eq_iff_heq` `Quiver.Path.obj_eq_of_cons_eq_cons` `Quiver.Path.cast_rfl_rfl` `Quiver.Path.heq_of_cons_eq_cons` `Quiver.Hom.cast_heq` `Quiver.Path.hom_heq_of_cons_eq_cons`
`pathStar_surjective` 📖	mathematical	`Quiver.Star` `obj` `star`	`Quiver.PathStar` `pathStar`	—	—
`star_apply` 📖	mathematical	—	`star` `obj` `map`	—	—
`star_comp` 📖	mathematical	—	`star` `comp` `Quiver.Star` `obj`	—	—
`star_fst` 📖	mathematical	—	`Quiver.Hom` `obj` `star`	—	—
`star_snd` 📖	mathematical	—	`Quiver.Hom` `obj` `star` `map`	—	—
`symmetrifyCostar` 📖	mathematical	—	`costar` `Quiver.Symmetrify` `Quiver.symmetrifyQuiver` `symmetrify` `Quiver.Costar` `obj` `Quiver.Symmetrify.of` `Quiver.Star` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Quiver.symmetrifyCostar` `star`	—	`Equiv.eq_symm_comp` `Equiv.sigmaSumDistrib_apply`
`symmetrifyStar` 📖	mathematical	—	`star` `Quiver.Symmetrify` `Quiver.symmetrifyQuiver` `symmetrify` `Quiver.Star` `obj` `Quiver.Symmetrify.of` `Quiver.Costar` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Quiver.symmetrifyStar` `costar`	—	`Equiv.eq_symm_comp` `Equiv.sigmaSumDistrib_apply`

Prefunctor.IsCovering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`Prefunctor.IsCovering`	`Prefunctor.comp`	—	`Function.Bijective.comp` `star_bijective` `costar_bijective`
`costar_bijective` 📖	mathematical	`Prefunctor.IsCovering`	`Function.Bijective` `Quiver.Costar` `Prefunctor.obj` `Prefunctor.costar`	—	—
`map_injective` 📖	mathematical	`Prefunctor.IsCovering`	`Quiver.Hom` `Prefunctor.obj` `Prefunctor.map`	—	`star_bijective`
`of_comp_left` 📖	—	`Prefunctor.IsCovering` `Prefunctor.comp` `Prefunctor.obj`	—	—	`Function.Bijective.of_comp_iff` `star_bijective` `costar_bijective`
`of_comp_right` 📖	—	`Prefunctor.IsCovering` `Prefunctor.comp`	—	—	`Function.Bijective.of_comp_iff'` `star_bijective` `costar_bijective`
`pathStar_bijective` 📖	mathematical	`Prefunctor.IsCovering`	`Function.Bijective` `Quiver.PathStar` `Prefunctor.obj` `Prefunctor.pathStar`	—	`Prefunctor.pathStar_bijective` `star_bijective`
`star_bijective` 📖	mathematical	`Prefunctor.IsCovering`	`Function.Bijective` `Quiver.Star` `Prefunctor.obj` `Prefunctor.star`	—	—
`symmetrify` 📖	mathematical	`Prefunctor.IsCovering`	`Quiver.Symmetrify` `Quiver.symmetrifyQuiver` `Prefunctor.symmetrify`	—	`Prefunctor.symmetrifyStar` `star_bijective` `costar_bijective` `Prefunctor.symmetrifyCostar`

Quiver

Definitions

Name	Category	Theorems
`Costar` 📖	CompOp	12 math math: `starEquivCostar_symm_apply_fst`, `starEquivCostar_apply_fst`, `starEquivCostar_apply_snd`, `Prefunctor.costar_comp`, `Prefunctor.costar_conj_star`, `starEquivCostar_symm_apply`, `Prefunctor.IsCovering.costar_bijective`, `Prefunctor.symmetrifyStar`, `starEquivCostar_apply`, `Prefunctor.symmetrifyCostar`, `starEquivCostar_symm_apply_snd`, `Prefunctor.bijective_costar_iff_bijective_star`
`PathStar` 📖	CompOp	4 math math: `Prefunctor.pathStar_surjective`, `Prefunctor.pathStar_injective`, `Prefunctor.IsCovering.pathStar_bijective`, `Prefunctor.pathStar_bijective`
`starEquivCostar` 📖	CompOp	7 math math: `starEquivCostar_symm_apply_fst`, `starEquivCostar_apply_fst`, `starEquivCostar_apply_snd`, `Prefunctor.costar_conj_star`, `starEquivCostar_symm_apply`, `starEquivCostar_apply`, `starEquivCostar_symm_apply_snd`
`symmetrifyCostar` 📖	CompOp	1 math math: `Prefunctor.symmetrifyCostar`
`symmetrifyStar` 📖	CompOp	1 math math: `Prefunctor.symmetrifyStar`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`starEquivCostar_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Star` `Costar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starEquivCostar` `reverse` `HasInvolutiveReverse.toHasReverse`	—	—
`starEquivCostar_apply_fst` 📖	mathematical	—	`Hom` `DFunLike.coe` `Equiv` `Star` `Costar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starEquivCostar`	—	—
`starEquivCostar_apply_snd` 📖	mathematical	—	`Hom` `DFunLike.coe` `Equiv` `Star` `Costar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starEquivCostar` `reverse` `HasInvolutiveReverse.toHasReverse`	—	—
`starEquivCostar_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Costar` `Star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `starEquivCostar` `reverse` `HasInvolutiveReverse.toHasReverse`	—	—
`starEquivCostar_symm_apply_fst` 📖	mathematical	—	`Hom` `DFunLike.coe` `Equiv` `Costar` `Star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `starEquivCostar`	—	—
`starEquivCostar_symm_apply_snd` 📖	mathematical	—	`Hom` `DFunLike.coe` `Equiv` `Costar` `Star` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `starEquivCostar` `reverse` `HasInvolutiveReverse.toHasReverse`	—	—

Quiver.Costar

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Quiver.PathStar

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Quiver.Star

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

---

← Back to Index