Documentation Verification Report

Functor

📁 Source: Mathlib/Data/Finset/Functor.lean

Statistics

Metric	Count
Definitions `applicative`, `functor`, `instAlternativeMonad`, `instMonad`, `pure`, `traverse`	6
Theorems `bind_def`, `commApplicative`, `fmap_def`, `id_traverse`, `image₂_def`, `instLawfulAlternative`, `instLawfulMonad`, `lawfulApplicative`, `lawfulFunctor`, `map_comp_coe`, `map_comp_coe_apply`, `map_traverse`, `pure_def`, `seqLeft_def`, `seqRight_def`, `seq_def`	16
Total	22

Finset

Definitions

Name	Category	Theorems
`applicative` 📖	CompOp	6 math math: `seqRight_def`, `seq_def`, `seqLeft_def`, `image₂_def`, `commApplicative`, `lawfulApplicative`
`functor` 📖	CompOp	5 math math: `map_traverse`, `image₂_def`, `map_comp_coe`, `lawfulFunctor`, `fmap_def`
`instAlternativeMonad` 📖	CompOp	1 math math: `instLawfulAlternative`
`instMonad` 📖	CompOp	2 math math: `bind_def`, `instLawfulMonad`
`pure` 📖	CompOp	1 math math: `pure_def`
`traverse` 📖	CompOp	2 math math: `map_traverse`, `id_traverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_def` 📖	mathematical	—	`Finset` `instMonad` `sup` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot`	—	—
`commApplicative` 📖	mathematical	—	`CommApplicative` `Finset` `applicative`	—	`lawfulApplicative` `sup_image` `sup_eq_biUnion` `product_eq_biUnion` `product_eq_biUnion_right`
`fmap_def` 📖	mathematical	—	`Finset` `functor` `image`	—	—
`id_traverse` 📖	mathematical	—	`traverse` `instCommApplicativeId` `Finset`	—	`instCommApplicativeId` `traverse.eq_1` `Multiset.id_traverse` `val_toFinset`
`image₂_def` 📖	mathematical	—	`image₂` `Finset` `applicative` `functor`	—	`ext` `sup_image`
`instLawfulAlternative` 📖	mathematical	—	`Finset` `instAlternativeMonad`	—	`lawfulApplicative` `image_empty` `sup_empty` `union_empty` `empty_union` `union_assoc` `image_union`
`instLawfulMonad` 📖	mathematical	—	`Finset` `instMonad`	—	`lawfulApplicative` `sup_singleton_apply` `sup_singleton` `sup_eq_biUnion` `biUnion_biUnion`
`lawfulApplicative` 📖	mathematical	—	`Finset` `applicative`	—	`lawfulFunctor` `seq_def` `fmap_def` `seqLeft_def` `eq_empty_or_nonempty` `sup_bot` `ext` `Nonempty.ne_empty` `mem_sup` `mem_image_of_mem` `mem_image_const_self` `mem_image` `seqRight_def` `image_empty` `sup_empty` `bot_eq_empty` `image_id` `sup_singleton` `image_singleton` `sup_singleton_apply`
`lawfulFunctor` 📖	mathematical	—	`Finset` `functor`	—	`image_id` `image_image`
`map_comp_coe` 📖	mathematical	—	`Multiset` `Finset` `functor` `Multiset.toFinset` `Multiset.functor`	—	`image_toFinset`
`map_comp_coe_apply` 📖	mathematical	—	`image` `Multiset.toFinset` `Multiset` `Multiset.functor`	—	`map_comp_coe`
`map_traverse` 📖	mathematical	—	`Finset` `functor` `traverse`	—	`CommApplicative.toLawfulApplicative` `map_comp_coe_apply`
`pure_def` 📖	mathematical	—	`Finset` `pure` `instSingleton`	—	—
`seqLeft_def` 📖	mathematical	—	`Finset` `applicative` `instEmptyCollection`	—	—
`seqRight_def` 📖	mathematical	—	`Finset` `applicative` `instEmptyCollection`	—	—
`seq_def` 📖	mathematical	—	`Finset` `applicative` `sup` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot` `image`	—	—

---

← Back to Index