Mem

📁 Source: Mathlib/Data/Vector/Mem.lean

Statistics

Metric	Count
Definitions Mem, Mem, Mem, Mem, Mem, Mem, Mem, Mem, Mem, Mem, Mem	11
Theorems get_mem, head_mem, mem_cons_iff, mem_cons_of_mem, mem_cons_self, mem_iff_get, mem_map_iff, mem_map_succ_iff, mem_of_mem_tail, mem_succ_iff, notMem_map_zero, notMem_nil, notMem_zero	13
Total	24

Class

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Computation

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Cycle

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

List.Vector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get_mem 📖	mathematical	—	toList get	—	—
head_mem 📖	mathematical	—	toList head	—	mem_iff_get get_zero
mem_cons_iff 📖	mathematical	—	toList cons	—	toList_cons
mem_cons_of_mem 📖	mathematical	toList	cons	—	mem_cons_iff
mem_cons_self 📖	mathematical	—	toList cons	—	mem_iff_get get_cons_zero
mem_iff_get 📖	mathematical	—	toList get	—	toList_length
mem_map_iff 📖	mathematical	—	toList map	—	toList_map
mem_map_succ_iff 📖	mathematical	—	toList map head tail	—	mem_succ_iff head_map tail_map mem_map_iff
mem_of_mem_tail 📖	—	toList tail	—	—	notMem_zero mem_succ_iff
mem_succ_iff 📖	mathematical	—	toList head tail	—	exists_eq_cons head_cons tail_cons
notMem_map_zero 📖	mathematical	—	toList map	—	eq_nil
notMem_nil 📖	mathematical	—	toList nil	—	toList_empty
notMem_zero 📖	mathematical	—	toList	—	notMem_nil eq_nil

Multiset

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

PSet

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Part

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Set

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Stream'.Seq

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Stream'.WSeq

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

Sym2

Definitions

Name	Category	Theorems
Mem 📖	MathDef	2 math math: mem_iff', mem_iff_mem

ZFSet

Definitions

Name	Category	Theorems
Mem 📖	MathDef	—

---

← Back to Index