Documentation Verification Report

Functor

📁 Source: Mathlib/Logic/Equiv/Functor.lean

Statistics

Metric	Count
Definitions `mapEquiv`, `mapEquiv`	2
Theorems `mapEquiv_apply`, `mapEquiv_refl_refl`, `mapEquiv_symm_apply`, `mapEquiv_apply`, `mapEquiv_refl`, `mapEquiv_symm_apply`	6
Total	8

Bifunctor

Definitions

Name	Category	Theorems
`mapEquiv` 📖	CompOp	3 math math: `mapEquiv_apply`, `mapEquiv_symm_apply`, `mapEquiv_refl_refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `bimap`	—	—
`mapEquiv_refl_refl` 📖	mathematical	—	`mapEquiv` `Equiv.refl`	—	`Equiv.Perm.ext` `LawfulBifunctor.id_bimap`
`mapEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapEquiv` `bimap`	—	—

Functor

Definitions

Name	Category	Theorems
`mapEquiv` 📖	CompOp	3 math math: `mapEquiv_refl`, `mapEquiv_symm_apply`, `mapEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv`	—	—
`mapEquiv_refl` 📖	mathematical	—	`mapEquiv` `Equiv.refl`	—	`Equiv.Perm.ext`
`mapEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapEquiv`	—	—

---

← Back to Index