Documentation Verification Report

Lists

📁 Source: Mathlib/SetTheory/Lists.lean

Statistics

Metric	Count
Definitions `Finsets`, `instDecidableEq`, `instEmptyCollection`, `instInhabited`, `Lists`, `Lists'`, `cons`, `instHasSubsetTrue`, `instInhabited`, `instMembershipLists`, `ofList`, `recOfList`, `toList`, `decidable`, `IsList`, `decidable`, `atom`, `inductionMut`, `instDecidableEq`, `instDecidableRelEquiv`, `instInhabited`, `instMembership`, `instSetoidLists`, `instSizeOf`, `mem`, `decidable`, `of'`, `ofList`, `toList`, `instDecidableEqLists'`, `decEq`	31
Theorems `refl`, `trans`, `cons_subset`, `mem_cons`, `mem_def`, `mem_equiv_left`, `mem_of_subset`, `mem_of_subset'`, `ofList_subset`, `of_toList`, `subset_def`, `subset_nil`, `toList_cons`, `to_ofList`, `antisymm_iff`, `trans`, `equiv_atom`, `isList_of_mem`, `isList_toList`, `lt_sizeof_cons'`, `of_toList`, `sizeof_pos`, `to_ofList`	23
Total	54

Finsets

Definitions

Name	Category	Theorems
`instDecidableEq` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	—
`instInhabited` 📖	CompOp	—

Lists

Definitions

Name	Category	Theorems
`IsList` 📖	MathDef	2 math math: `isList_toList`, `isList_of_mem`
`atom` 📖	CompOp	1 math math: `equiv_atom`
`inductionMut` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDecidableRelEquiv` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMembership` 📖	CompOp	—
`instSetoidLists` 📖	CompOp	—
`instSizeOf` 📖	CompOp	—
`mem` 📖	MathDef	—
`of'` 📖	CompOp	1 math math: `Equiv.antisymm_iff`
`ofList` 📖	CompOp	3 math math: `to_ofList`, `of_toList`, `isList_toList`
`toList` 📖	CompOp	2 math math: `to_ofList`, `of_toList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_atom` 📖	mathematical	—	`Equiv` `atom`	—	—
`isList_of_mem` 📖	mathematical	`Lists` `instMembership`	`IsList`	—	—
`isList_toList` 📖	mathematical	—	`IsList` `ofList`	—	—
`lt_sizeof_cons'` 📖	mathematical	—	`Lists'` `Lists'.cons'`	—	`IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `sizeof_pos`
`of_toList` 📖	mathematical	`IsList`	`ofList` `toList`	—	`Lists'.of_toList`
`sizeof_pos` 📖	mathematical	—	`Lists'`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass`
`to_ofList` 📖	mathematical	—	`toList` `ofList`	—	`Lists'.to_ofList`

Lists'

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	3 math math: `toList_cons`, `cons_subset`, `mem_cons`
`instHasSubsetTrue` 📖	CompOp	5 math math: `subset_def`, `Subset.refl`, `cons_subset`, `ofList_subset`, `Lists.Equiv.antisymm_iff`
`instInhabited` 📖	CompOp	—
`instMembershipLists` 📖	CompOp	6 math math: `mem_equiv_left`, `mem_def`, `subset_def`, `cons_subset`, `mem_of_subset'`, `mem_cons`
`ofList` 📖	CompOp	3 math math: `to_ofList`, `ofList_subset`, `of_toList`
`recOfList` 📖	CompOp	—
`toList` 📖	CompOp	4 math math: `toList_cons`, `mem_def`, `to_ofList`, `of_toList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_subset` 📖	mathematical	—	`Lists'` `instHasSubsetTrue` `cons` `Lists` `instMembershipLists`	—	—
`mem_cons` 📖	mathematical	—	`Lists` `Lists'` `instMembershipLists` `cons` `Lists.Equiv`	—	—
`mem_def` 📖	mathematical	—	`Lists` `Lists'` `instMembershipLists` `toList` `Lists.Equiv`	—	—
`mem_equiv_left` 📖	mathematical	`Lists.Equiv`	`Lists` `Lists'` `instMembershipLists`	—	`Lists.Equiv.trans` `Lists.Equiv.symm`
`mem_of_subset` 📖	—	`Lists'` `instHasSubsetTrue` `Lists` `instMembershipLists`	—	—	`mem_equiv_left` `mem_of_subset'`
`mem_of_subset'` 📖	mathematical	`Lists'` `instHasSubsetTrue` `Lists` `toList`	`instMembershipLists`	—	—
`ofList_subset` 📖	mathematical	`Lists`	`Lists'` `instHasSubsetTrue` `ofList`	—	`to_ofList`
`of_toList` 📖	mathematical	—	`ofList` `toList`	—	—
`subset_def` 📖	mathematical	—	`Lists'` `instHasSubsetTrue` `Lists` `instMembershipLists`	—	`mem_of_subset'` `cons_subset` `to_ofList`
`subset_nil` 📖	—	`Lists'` `instHasSubsetTrue` `nil`	—	—	`of_toList` `cons_subset`
`toList_cons` 📖	mathematical	—	`toList` `cons` `Lists`	—	—
`to_ofList` 📖	mathematical	—	`toList` `ofList`	—	—

Lists'.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Lists'` `Lists'.instHasSubsetTrue`	—	`Lists'.of_toList` `Lists'.ofList_subset`
`trans` 📖	—	`Lists'` `Lists'.instHasSubsetTrue`	—	—	`Lists'.subset_def` `Lists'.mem_of_subset` `Lists'.mem_of_subset'`

Lists.Equiv

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm_iff` 📖	mathematical	—	`Lists.Equiv` `Lists.of'` `Lists'` `Lists'.instHasSubsetTrue`	—	—
`trans` 📖	—	`Lists.Equiv`	—	—	`Lists.equiv_atom` `antisymm_iff` `Lists'.subset_def` `Lists'.mem_of_subset'` `symm`

Lists.Subset

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Lists.mem

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Finsets` 📖	CompOp	—
`Lists` 📖	CompOp	6 math math: `Lists'.toList_cons`, `Lists'.mem_equiv_left`, `Lists'.mem_def`, `Lists'.subset_def`, `Lists'.cons_subset`, `Lists'.mem_cons`
`Lists'` 📖	CompData	10 math math: `Lists'.mem_equiv_left`, `Lists.lt_sizeof_cons'`, `Lists'.mem_def`, `Lists'.subset_def`, `Lists'.Subset.refl`, `Lists'.cons_subset`, `Lists'.ofList_subset`, `Lists'.mem_cons`, `Lists.sizeof_pos`, `Lists.Equiv.antisymm_iff`
`instDecidableEqLists'` 📖	CompOp	—

instDecidableEqLists'

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index