Documentation Verification Report

Functor

📁 Source: Mathlib/Control/Functor.lean

Statistics

Metric	Count
Definitions `AddConst`, `functor`, `mk`, `run`, `functor`, `instApplicativeComp`, `instInhabited`, `instPure`, `instSeq`, `map`, `mk`, `run`, `seq`, `functor`, `instInhabited`, `map`, `mk`, `mk'`, `run`, `Liftp`, `Liftr`, `instInhabitedAddConst`, `mapConstRev`, `supp`, `«term_$>_»`	25
Theorems `lawfulFunctor`, `comp_map`, `ext`, `functor_comp_id`, `functor_id_comp`, `id_map`, `lawfulFunctor`, `map_mk`, `run_map`, `run_pure`, `run_seq`, `ext`, `lawfulFunctor`, `ext`, `map_comp_map`, `map_id`, `of_mem_supp`	17
Total	42

Functor

Definitions

Name	Category	Theorems
`AddConst` 📖	CompOp	2 math math: `AddConst.lawfulFunctor`, `instLawfulApplicativeAddConst`
`Liftp` 📖	MathDef	6 math math: `QPF.liftp_iff'`, `QPF.liftp_iff_of_isUniform`, `PFunctor.liftp_iff`, `QPF.has_good_supp_iff`, `PFunctor.liftp_iff'`, `QPF.liftp_iff`
`Liftr` 📖	MathDef	2 math math: `QPF.liftr_iff`, `PFunctor.liftr_iff`
`instInhabitedAddConst` 📖	CompOp	—
`mapConstRev` 📖	CompOp	—
`supp` 📖	CompOp	5 math math: `PFunctor.supp_eq`, `QPF.supp_eq`, `QPF.supp_map`, `QPF.mem_supp`, `QPF.supp_eq_of_isUniform`
`«term_$>_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—
`map_comp_map` 📖	—	—	—	—	—
`map_id` 📖	—	—	—	—	—
`of_mem_supp` 📖	—	`Liftp` `Set` `Set.instMembership` `supp`	—	—	—

Functor.AddConst

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	1 math math: `lawfulFunctor`
`mk` 📖	CompOp	—
`run` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lawfulFunctor` 📖	mathematical	—	`Functor.AddConst` `functor`	—	`Functor.Const.lawfulFunctor`

Functor.Comp

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	9 math math: `map_pure`, `seq_pure`, `functor_id_comp`, `pure_seq_eq_map`, `functor_comp_id`, `run_map`, `seq_assoc`, `map_mk`, `lawfulFunctor`
`instApplicativeComp` 📖	CompOp	24 math math: `LawfulBitraversable.comp_bitraverse`, `Bitraversable.tfst_comp_tfst`, `applicative_comp_id`, `LawfulTraversable.comp_traverse`, `applicative_id_comp`, `Bitraversable.tsnd_comp_tfst`, `Bitraversable.tfst_tsnd`, `Multiset.comp_traverse`, `Bitraversable.comp_tsnd`, `Equiv.comp_traverse`, `Traversable.comp_sequence`, `Sum.comp_traverse`, `instCommApplicative`, `Bitraversable.tsnd_comp_tsnd`, `Option.comp_traverse`, `LawfulBitraversable.bitraverse_comp`, `Bitraversable.tfst_comp_tsnd`, `List.comp_traverse`, `Bitraversable.tsnd_tfst`, `Traversable.traverse_comp`, `List.Vector.comp_traverse`, `Bitraversable.comp_tfst`, `instLawfulApplicativeComp`, `Tree.comp_traverse`
`instInhabited` 📖	CompOp	—
`instPure` 📖	CompOp	4 math math: `map_pure`, `seq_pure`, `pure_seq_eq_map`, `run_pure`
`instSeq` 📖	CompOp	5 math math: `run_seq`, `seq_pure`, `pure_seq_eq_map`, `seq_assoc`, `Comp.seq_mk`
`map` 📖	CompOp	2 math math: `id_map`, `comp_map`
`mk` 📖	CompOp	—
`run` 📖	CompOp	3 math math: `run_seq`, `run_pure`, `run_map`
`seq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_map` 📖	mathematical	—	`map`	—	—
`ext` 📖	—	`run`	—	—	—
`functor_comp_id` 📖	mathematical	—	`functor`	—	`Functor.ext` `lawfulFunctor`
`functor_id_comp` 📖	mathematical	—	`functor`	—	`Functor.ext` `lawfulFunctor`
`id_map` 📖	mathematical	—	`map`	—	—
`lawfulFunctor` 📖	mathematical	—	`Functor.Comp` `functor`	—	`id_map` `comp_map`
`map_mk` 📖	mathematical	—	`Functor.Comp` `functor`	—	—
`run_map` 📖	mathematical	—	`run` `Functor.Comp` `functor`	—	—
`run_pure` 📖	mathematical	—	`run` `Functor.Comp` `instPure`	—	—
`run_seq` 📖	mathematical	—	`run` `Functor.Comp` `instSeq`	—	—

Functor.Const

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	1 math math: `lawfulFunctor`
`instInhabited` 📖	CompOp	—
`map` 📖	CompOp	—
`mk` 📖	CompOp	—
`mk'` 📖	CompOp	—
`run` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`run`	—	—	—
`lawfulFunctor` 📖	mathematical	—	`Functor.Const` `functor`	—	—

---

← Back to Index