Documentation Verification Report

EquivFunctor

📁 Source: Mathlib/Control/EquivFunctor.lean

Statistics

Metric	Count
Definitions `EquivFunctor`, `map`, `mapEquiv`, `ofLawfulFunctor`	4
Theorems `injective`, `mapEquiv_apply`, `mapEquiv_refl`, `mapEquiv_symm`, `mapEquiv_symm_apply`, `mapEquiv_trans`, `map_refl'`, `map_trans'`	8
Total	12

EquivFunctor

Definitions

Name	Category	Theorems
`map` 📖	CompOp	4 math math: `map_trans'`, `mapEquiv_apply`, `map_refl'`, `mapEquiv_symm_apply`
`mapEquiv` 📖	CompOp	7 math math: `mapEquiv_symm`, `mapEquiv_refl`, `mapEquiv_apply`, `mapEquiv.injective`, `mapEquiv_trans`, `mapEquiv_symm_apply`, `Equiv.optionCongr_eq_equivFunctor_mapEquiv`
`ofLawfulFunctor` 📖	CompOp	2 math math: `mapEquiv.injective`, `Equiv.optionCongr_eq_equivFunctor_mapEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `map`	—	—
`mapEquiv_refl` 📖	mathematical	—	`mapEquiv` `Equiv.refl`	—	`Equiv.Perm.ext` `map_refl'`
`mapEquiv_symm` 📖	mathematical	—	`Equiv.symm` `mapEquiv`	—	`Equiv.ext` `mapEquiv_symm_apply`
`mapEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapEquiv` `map`	—	—
`mapEquiv_trans` 📖	mathematical	—	`Equiv.trans` `mapEquiv`	—	`Equiv.ext` `map_trans'`
`map_refl'` 📖	mathematical	—	`map` `Equiv.refl`	—	—
`map_trans'` 📖	mathematical	—	`map` `Equiv.trans`	—	—

EquivFunctor.mapEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective` 📖	mathematical	—	`Equiv` `EquivFunctor.mapEquiv` `EquivFunctor.ofLawfulFunctor`	—	`Equiv.ext` `Equiv.congr_fun`

(root)

Definitions

Name	Category	Theorems
`EquivFunctor` 📖	CompData	—

---

← Back to Index