Documentation Verification Report

Equiv

📁 Source: Mathlib/Topology/Homotopy/Equiv.lean

Statistics

Metric	Count
Definitions `HomotopyEquiv`, `apply`, `symm_apply`, `instCoeFunForall`, `instInhabitedUnit`, `invFun`, `piCongrRight`, `prodCongr`, `refl`, `toFun`, `trans`, `«term_≃ₕ_»`, `toHomotopyEquiv`	13
Theorems `coe_invFun`, `continuous`, `ext`, `ext_iff`, `left_inv`, `refl_apply`, `refl_symm_apply`, `right_inv`, `symm_trans`, `trans_apply`, `trans_symm_apply`, `coe_toHomotopyEquiv`, `refl_toHomotopyEquiv`, `symm_toHomotopyEquiv`, `trans_toHomotopyEquiv`	15
Total	28

ContinuousMap

Definitions

Name	Category	Theorems
`HomotopyEquiv` 📖	CompData	3 math math: `ContractibleSpace.hequiv_unit`, `ContractibleSpace.hequiv`, `ContractibleSpace.hequiv_unit'`
`«term_≃ₕ_»` 📖	CompOp	—

ContinuousMap.HomotopyEquiv

Definitions

Name	Category	Theorems
`instCoeFunForall` 📖	CompOp	—
`instInhabitedUnit` 📖	CompOp	—
`invFun` 📖	CompOp	4 math math: `right_inv`, `ext_iff`, `left_inv`, `coe_invFun`
`piCongrRight` 📖	CompOp	—
`prodCongr` 📖	CompOp	—
`refl` 📖	CompOp	3 math math: `refl_symm_apply`, `Homeomorph.refl_toHomotopyEquiv`, `refl_apply`
`toFun` 📖	CompOp	10 math math: `refl_symm_apply`, `right_inv`, `ext_iff`, `trans_apply`, `left_inv`, `coe_invFun`, `Homeomorph.coe_toHomotopyEquiv`, `continuous`, `trans_symm_apply`, `refl_apply`
`trans` 📖	CompOp	4 math math: `trans_apply`, `Homeomorph.trans_toHomotopyEquiv`, `symm_trans`, `trans_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_invFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `invFun` `toFun` `symm`	—	—
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toFun`	—	`ContinuousMap.continuous`
`ext` 📖	—	`toFun` `invFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun` `invFun`	—	`ext`
`left_inv` 📖	mathematical	—	`ContinuousMap.Homotopic` `ContinuousMap.comp` `invFun` `toFun` `ContinuousMap.id`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toFun` `refl`	—	—
`refl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toFun` `symm` `refl`	—	—
`right_inv` 📖	mathematical	—	`ContinuousMap.Homotopic` `ContinuousMap.comp` `toFun` `invFun` `ContinuousMap.id`	—	—
`symm_trans` 📖	mathematical	—	`symm` `trans`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toFun` `trans`	—	—
`trans_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toFun` `symm` `trans`	—	—

ContinuousMap.HomotopyEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

Homeomorph

Definitions

Name	Category	Theorems
`toHomotopyEquiv` 📖	CompOp	4 math math: `symm_toHomotopyEquiv`, `refl_toHomotopyEquiv`, `coe_toHomotopyEquiv`, `trans_toHomotopyEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHomotopyEquiv` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `ContinuousMap.HomotopyEquiv.toFun` `toHomotopyEquiv` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—
`refl_toHomotopyEquiv` 📖	mathematical	—	`toHomotopyEquiv` `refl` `ContinuousMap.HomotopyEquiv.refl`	—	—
`symm_toHomotopyEquiv` 📖	mathematical	—	`toHomotopyEquiv` `symm` `ContinuousMap.HomotopyEquiv.symm`	—	—
`trans_toHomotopyEquiv` 📖	mathematical	—	`toHomotopyEquiv` `trans` `ContinuousMap.HomotopyEquiv.trans`	—	—

---

← Back to Index