List

📁 Source: Mathlib/Logic/Equiv/List.lean

Statistics

Metric	Count
Definitions denumerableList, decodeList, encodableOfList, encodeList, listEquivOfEquiv, listEquivSelfOfEquivNat, listNatEquivNat, listUniqueEquiv, toEncodable, truncEncodable, encodable	11
Theorems denumerable_list_aux, list_ofNat_succ, list_ofNat_zero, decodeList_encodeList_eq_self, decode_list_succ, decode_list_zero, encode_list_cons, encode_list_nil, length_le_encode, listUniqueEquiv_apply, listUniqueEquiv_symm_apply, countable, countable, countable	14
Total	25

Denumerable

Definitions

Name	Category	Theorems
denumerableList 📖	CompOp	2 math math: list_ofNat_succ, list_ofNat_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denumerable_list_aux 📖	mathematical	—	Encodable.decodeList toEncodable Encodable.encodeList	—	Encodable.decodeList.eq_1 Nat.unpair_right_le Encodable.decodeList.eq_2 decode_eq_ofNat encode_ofNat Nat.pair_eq_of_unpair_eq
list_ofNat_succ 📖	mathematical	—	ofNat denumerableList Nat.unpair	—	ofNat_of_decode Nat.unpair_right_le Encodable.decodeList.eq_2 decode_eq_ofNat Option.seq_some
list_ofNat_zero 📖	mathematical	—	ofNat denumerableList	—	Encodable.encode_list_nil ofNat_encode

Encodable

Definitions

Name	Category	Theorems
decodeList 📖	CompOp	2 math math: decodeList_encodeList_eq_self, Denumerable.denumerable_list_aux
encodableOfList 📖	CompOp	—
encodeList 📖	CompOp	2 math math: decodeList_encodeList_eq_self, Denumerable.denumerable_list_aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decodeList_encodeList_eq_self 📖	mathematical	—	decodeList encodeList	—	Nat.unpair_right_le decodeList.eq_2 Nat.unpair_pair encodek
decode_list_succ 📖	mathematical	—	decode List.encodable Nat.unpair	—	Nat.unpair_right_le decodeList.eq_2
decode_list_zero 📖	mathematical	—	decode List.encodable	—	decodeList.eq_1
encode_list_cons 📖	mathematical	—	encode List.encodable Nat.pair	—	—
encode_list_nil 📖	mathematical	—	encode List.encodable	—	—
length_le_encode 📖	mathematical	—	encode List.encodable	—	LE.le.trans Nat.right_le_pair

Equiv

Definitions

Name	Category	Theorems
listEquivOfEquiv 📖	CompOp	—
listEquivSelfOfEquivNat 📖	CompOp	—
listNatEquivNat 📖	CompOp	—
listUniqueEquiv 📖	CompOp	2 math math: listUniqueEquiv_apply, listUniqueEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
listUniqueEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike listUniqueEquiv	—	—
listUniqueEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm listUniqueEquiv Unique.instInhabited	—	—

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable Finset	—	Function.Injective.countable Multiset.countable val_injective

Fintype

Definitions

Name	Category	Theorems
toEncodable 📖	CompOp	—
truncEncodable 📖	CompOp	—

List

Definitions

Name	Category	Theorems
encodable 📖	CompOp	5 math math: Encodable.encode_list_nil, Encodable.decode_list_zero, Encodable.length_le_encode, Encodable.encode_list_cons, Encodable.decode_list_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Encodable.countable

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable Multiset	—	Quotient.countable List.countable

---

← Back to Index