Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions `PureTransformation`	1
Theorems `comp_sequence`, `id_sequence`, `map_eq_traverse_id`, `map_traverse`, `map_traverse'`, `naturality'`, `naturality_pf`, `pureTransformation_apply`, `pure_traverse`, `traverse_comp`, `traverse_eq_map_id'`, `traverse_id`, `traverse_map`, `traverse_map'`	14
Total	15

Traversable

Definitions

Name	Category	Theorems
`PureTransformation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_sequence` 📖	mathematical	—	`sequence` `Functor.Comp` `Functor.Comp.instApplicativeComp` `toFunctor`	—	`traverse_map` `Functor.Comp.instLawfulApplicativeComp` `LawfulTraversable.comp_traverse` `Functor.map_id`
`id_sequence` 📖	mathematical	—	`sequence` `toFunctor`	—	`traverse_map` `CommApplicative.toLawfulApplicative` `instCommApplicativeId` `LawfulTraversable.id_traverse`
`map_eq_traverse_id` 📖	mathematical	—	`toFunctor` `traverse`	—	`LawfulTraversable.traverse_eq_map_id`
`map_traverse` 📖	mathematical	—	`toFunctor` `traverse`	—	`map_eq_traverse_id` `LawfulTraversable.comp_traverse` `CommApplicative.toLawfulApplicative` `instCommApplicativeId` `Functor.Comp.applicative_comp_id`
`map_traverse'` 📖	mathematical	—	`traverse` `toFunctor`	—	`map_traverse`
`naturality'` 📖	mathematical	—	`sequence` `toFunctor`	—	`LawfulTraversable.naturality` `traverse_map`
`naturality_pf` 📖	mathematical	—	`traverse`	—	`LawfulTraversable.naturality`
`pureTransformation_apply` 📖	—	—	—	—	—
`pure_traverse` 📖	mathematical	—	`traverse`	—	`LawfulTraversable.naturality` `CommApplicative.toLawfulApplicative` `instCommApplicativeId` `LawfulTraversable.id_traverse`
`traverse_comp` 📖	mathematical	—	`traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`LawfulTraversable.comp_traverse`
`traverse_eq_map_id'` 📖	mathematical	—	`traverse` `toFunctor`	—	`LawfulTraversable.traverse_eq_map_id`
`traverse_id` 📖	mathematical	—	`traverse`	—	`LawfulTraversable.id_traverse`
`traverse_map` 📖	mathematical	—	`traverse` `toFunctor`	—	`map_eq_traverse_id` `LawfulTraversable.comp_traverse` `CommApplicative.toLawfulApplicative` `instCommApplicativeId` `Functor.Comp.applicative_id_comp`
`traverse_map'` 📖	mathematical	—	`traverse` `toFunctor`	—	`traverse_map`

---

← Back to Index