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, instDecidableEquiv, instDecidableMemLists'True, instDecidableRelEquiv, instDecidableSubsetLists'True, instInhabited, instMembership, instSetoidLists, instSizeOf, mem, decidable, of', ofList, toList, instDecidableEqLists', decEq	34
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	57

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	—
instDecidableEquiv 📖	CompOp	—
instDecidableMemLists'True 📖	CompOp	—
instDecidableRelEquiv 📖	CompOp	—
instDecidableSubsetLists'True 📖	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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	6 math math: subset_def, Subset.refl, Subset.trans, cons_subset, ofList_subset, Lists.Equiv.antisymm_iff
instInhabited 📖	CompOp	—
instMembershipLists 📖	CompOp	7 math math: mem_equiv_left, mem_def, subset_def, mem_of_subset, 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 📖	mathematical	Lists' instHasSubsetTrue Lists instMembershipLists	Lists Lists' instMembershipLists	—	mem_equiv_left mem_of_subset'
mem_of_subset' 📖	mathematical	Lists' instHasSubsetTrue Lists toList	Lists Lists' 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 📖	mathematical	Lists' instHasSubsetTrue nil	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 📖	mathematical	Lists' Lists'.instHasSubsetTrue	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 📖	mathematical	Lists.Equiv	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	8 math math: Lists'.toList_cons, Lists'.mem_equiv_left, Lists'.mem_def, Lists'.subset_def, Lists'.mem_of_subset, Lists'.cons_subset, Lists'.mem_of_subset', Lists'.mem_cons
Lists' 📖	CompData	13 math math: Lists'.mem_equiv_left, Lists.lt_sizeof_cons', Lists'.mem_def, Lists'.subset_def, Lists'.Subset.refl, Lists'.mem_of_subset, Lists'.Subset.trans, Lists'.cons_subset, Lists'.ofList_subset, Lists'.mem_of_subset', Lists'.mem_cons, Lists.sizeof_pos, Lists.Equiv.antisymm_iff
instDecidableEqLists' 📖	CompOp	—

instDecidableEqLists'

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index