Documentation Verification Report

Lemmas

📁 Source: Mathlib/Control/Bitraversable/Lemmas.lean

Statistics

Metric	Count
Definitions `tfst`, `tsnd`	2
Theorems `comp_tfst`, `comp_tsnd`, `id_tfst`, `id_tsnd`, `tfst_comp_tfst`, `tfst_comp_tsnd`, `tfst_eq_fst_id`, `tfst_eq_fst_id'`, `tfst_id`, `tfst_tsnd`, `tsnd_comp_tfst`, `tsnd_comp_tsnd`, `tsnd_eq_snd_id`, `tsnd_eq_snd_id'`, `tsnd_id`, `tsnd_tfst`	16
Total	18

Bitraversable

Definitions

Name	Category	Theorems
`tfst` 📖	CompOp	10 math math: `tfst_comp_tfst`, `id_tfst`, `tsnd_comp_tfst`, `tfst_tsnd`, `tfst_id`, `tfst_comp_tsnd`, `tsnd_tfst`, `tfst_eq_fst_id`, `comp_tfst`, `tfst_eq_fst_id'`
`tsnd` 📖	CompOp	10 math math: `tsnd_id`, `tsnd_comp_tfst`, `tfst_tsnd`, `comp_tsnd`, `tsnd_comp_tsnd`, `id_tsnd`, `tsnd_eq_snd_id'`, `tfst_comp_tsnd`, `tsnd_tfst`, `tsnd_eq_snd_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tfst` 📖	mathematical	—	`tfst` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`LawfulBitraversable.comp_bitraverse`
`comp_tsnd` 📖	mathematical	—	`tsnd` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`LawfulBitraversable.comp_bitraverse`
`id_tfst` 📖	mathematical	—	`tfst`	—	`LawfulBitraversable.id_bitraverse`
`id_tsnd` 📖	mathematical	—	`tsnd`	—	`LawfulBitraversable.id_bitraverse`
`tfst_comp_tfst` 📖	mathematical	—	`Functor.Comp` `tfst` `Functor.Comp.instApplicativeComp`	—	`comp_tfst`
`tfst_comp_tsnd` 📖	mathematical	—	`Functor.Comp` `tfst` `tsnd` `bitraverse` `Functor.Comp.instApplicativeComp`	—	`tfst_tsnd`
`tfst_eq_fst_id` 📖	mathematical	—	`tfst` `Bifunctor.fst` `toBifunctor`	—	`LawfulBitraversable.bitraverse_eq_bimap_id`
`tfst_eq_fst_id'` 📖	mathematical	—	`tfst` `Bifunctor.fst` `toBifunctor`	—	`tfst_eq_fst_id`
`tfst_id` 📖	mathematical	—	`tfst`	—	`id_tfst`
`tfst_tsnd` 📖	mathematical	—	`tfst` `tsnd` `bitraverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`LawfulBitraversable.comp_bitraverse`
`tsnd_comp_tfst` 📖	mathematical	—	`Functor.Comp` `tsnd` `tfst` `bitraverse` `Functor.Comp.instApplicativeComp`	—	`tsnd_tfst`
`tsnd_comp_tsnd` 📖	mathematical	—	`Functor.Comp` `tsnd` `Functor.Comp.instApplicativeComp`	—	`comp_tsnd`
`tsnd_eq_snd_id` 📖	mathematical	—	`tsnd` `Bifunctor.snd` `toBifunctor`	—	`LawfulBitraversable.bitraverse_eq_bimap_id`
`tsnd_eq_snd_id'` 📖	mathematical	—	`tsnd` `Bifunctor.snd` `toBifunctor`	—	`tsnd_eq_snd_id`
`tsnd_id` 📖	mathematical	—	`tsnd`	—	`id_tsnd`
`tsnd_tfst` 📖	mathematical	—	`tsnd` `tfst` `bitraverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`LawfulBitraversable.comp_bitraverse`

---

← Back to Index