Sort

📁 Source: Mathlib/Deprecated/Sort.lean

Statistics

Metric	Count
Definitions Sorted, decidableSorted	2
Theorems filter, filterMap, of_cons, rel_of_mem_take_of_mem_drop, tail, rel_of_sorted_cons, sorted_cons, sorted_nil, sorted_singleton	9
Total	11

List

Definitions

Name	Category	Theorems
Sorted 📖	MathDef	3 math math: sorted_nil, sorted_cons, sorted_singleton
decidableSorted 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rel_of_sorted_cons 📖	—	Sorted	—	—	—
sorted_cons 📖	mathematical	—	Sorted	—	—
sorted_nil 📖	mathematical	—	Sorted	—	—
sorted_singleton 📖	mathematical	—	Sorted	—	—

List.Sorted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
filter 📖	—	List.Sorted	—	—	—
filterMap 📖	—	List.Sorted	—	—	—
of_cons 📖	—	List.Sorted	—	—	—
rel_of_mem_take_of_mem_drop 📖	—	List.Sorted	—	—	—
tail 📖	—	List.Sorted	—	—	—

---

← Back to Index