Documentation Verification Report

Constructions

📁 Source: Mathlib/Data/W/Constructions.lean

Statistics

Metric	Count
Definitions `Listα`, `ListαEquivPUnitSum`, `Listβ`, `Natα`, `NatαEquivPUnitSumPUnit`, `Natβ`, `equivList`, `equivNat`, `instInhabitedListα`, `instInhabitedListβCons`, `instInhabitedNatα`, `instInhabitedNatβSucc`, `ofList`, `ofNat`, `toList`, `toNat`	16
Theorems `NatαEquivPUnitSumPUnit_apply`, `NatαEquivPUnitSumPUnit_symm_apply`, `leftInverse_list`, `leftInverse_nat`, `rightInverse_list`, `rightInverse_nat`	6
Total	22

WType

Definitions

Name	Category	Theorems
`Listα` 📖	CompData	2 math math: `leftInverse_list`, `rightInverse_list`
`ListαEquivPUnitSum` 📖	CompOp	—
`Listβ` 📖	CompOp	2 math math: `leftInverse_list`, `rightInverse_list`
`Natα` 📖	CompData	4 math math: `NatαEquivPUnitSumPUnit_apply`, `leftInverse_nat`, `rightInverse_nat`, `NatαEquivPUnitSumPUnit_symm_apply`
`NatαEquivPUnitSumPUnit` 📖	CompOp	2 math math: `NatαEquivPUnitSumPUnit_apply`, `NatαEquivPUnitSumPUnit_symm_apply`
`Natβ` 📖	CompOp	2 math math: `leftInverse_nat`, `rightInverse_nat`
`equivList` 📖	CompOp	—
`equivNat` 📖	CompOp	—
`instInhabitedListα` 📖	CompOp	—
`instInhabitedListβCons` 📖	CompOp	—
`instInhabitedNatα` 📖	CompOp	—
`instInhabitedNatβSucc` 📖	CompOp	—
`ofList` 📖	CompOp	2 math math: `leftInverse_list`, `rightInverse_list`
`ofNat` 📖	CompOp	2 math math: `leftInverse_nat`, `rightInverse_nat`
`toList` 📖	CompOp	2 math math: `leftInverse_list`, `rightInverse_list`
`toNat` 📖	CompOp	2 math math: `leftInverse_nat`, `rightInverse_nat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`NatαEquivPUnitSumPUnit_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Natα` `EquivLike.toFunLike` `Equiv.instEquivLike` `NatαEquivPUnitSumPUnit`	—	—
`NatαEquivPUnitSumPUnit_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Natα` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `NatαEquivPUnitSumPUnit` `Natα.zero` `Natα.succ`	—	—
`leftInverse_list` 📖	mathematical	—	`WType` `Listα` `Listβ` `ofList` `toList`	—	—
`leftInverse_nat` 📖	mathematical	—	`WType` `Natα` `Natβ` `ofNat` `toNat`	—	`toNat.eq_1` `ofNat.eq_1`
`rightInverse_list` 📖	mathematical	—	`WType` `Listα` `Listβ` `ofList` `toList`	—	—
`rightInverse_nat` 📖	mathematical	—	`WType` `Natα` `Natβ` `ofNat` `toNat`	—	`ofNat.eq_2` `toNat.eq_2`

---

← Back to Index