Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `WType`, `depth`, `elim`, `equivSigma`, `instEncodable`, `ofSigma`, `toSigma`, `instInhabitedWTypeUnitEmpty`	8
Theorems `depth_lt_depth_mk`, `depth_pos`, `elim_injective`, `equivSigma_apply`, `equivSigma_symm_apply`, `infinite_of_nonempty_of_isEmpty`, `instIsEmpty`, `ofSigma_toSigma`, `toSigma_ofSigma`	9
Total	17

WType

Definitions

Name	Category	Theorems
`depth` 📖	CompOp	2 math math: `depth_pos`, `depth_lt_depth_mk`
`elim` 📖	CompOp	1 math math: `elim_injective`
`equivSigma` 📖	CompOp	2 math math: `equivSigma_apply`, `equivSigma_symm_apply`
`instEncodable` 📖	CompOp	—
`ofSigma` 📖	CompOp	3 math math: `ofSigma_toSigma`, `toSigma_ofSigma`, `equivSigma_symm_apply`
`toSigma` 📖	CompOp	3 math math: `equivSigma_apply`, `ofSigma_toSigma`, `toSigma_ofSigma`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`depth_lt_depth_mk` 📖	mathematical	—	`depth`	—	`Finset.le_sup` `Finset.mem_univ`
`depth_pos` 📖	mathematical	—	`depth`	—	—
`elim_injective` 📖	mathematical	—	`WType` `elim`	—	—
`equivSigma_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WType` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSigma` `toSigma`	—	—
`equivSigma_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSigma` `ofSigma`	—	—
`infinite_of_nonempty_of_isEmpty` 📖	mathematical	—	`Infinite` `WType`	—	`not_injective_infinite_finite` `instInfiniteNat`
`instIsEmpty` 📖	mathematical	—	`IsEmpty` `WType`	—	—
`ofSigma_toSigma` 📖	mathematical	—	`ofSigma` `toSigma`	—	—
`toSigma_ofSigma` 📖	mathematical	—	`toSigma` `ofSigma`	—	—

(root)

Definitions

Name	Category	Theorems
`WType` 📖	CompData	15 math math: `WType.infinite_of_nonempty_of_isEmpty`, `WType.equivSigma_apply`, `WType.cardinalMk_le_max_aleph0_of_finite'`, `WType.leftInverse_list`, `WType.cardinalMk_eq_sum_lift`, `WType.cardinalMk_le_max_aleph0_of_finite`, `WType.elim_injective`, `WType.cardinalMk_eq_sum`, `WType.rightInverse_list`, `WType.equivSigma_symm_apply`, `WType.instIsEmpty`, `WType.cardinalMk_le_of_le'`, `WType.cardinalMk_le_of_le`, `WType.leftInverse_nat`, `WType.rightInverse_nat`
`instInhabitedWTypeUnitEmpty` 📖	CompOp	—

---

← Back to Index