ReduceOption

📁 Source: Mathlib/Data/List/ReduceOption.lean

Statistics

Metric	Count
Definitions	0
Theorems length_eq_reduceOption_length_add_filter_none, reduceOption_append, reduceOption_concat, reduceOption_concat_of_some, reduceOption_cons_of_none, reduceOption_cons_of_some, reduceOption_eq_append_iff, reduceOption_eq_concat_iff, reduceOption_eq_nil_iff, reduceOption_eq_singleton_iff, reduceOption_getElem?_iff, reduceOption_length_eq, reduceOption_length_eq_iff, reduceOption_length_le, reduceOption_length_lt_iff, reduceOption_map, reduceOption_mem_iff, reduceOption_nil, reduceOption_replicate_none, reduceOption_singleton	20
Total	20

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_eq_reduceOption_length_add_filter_none 📖	—	—	—	—	reduceOption_length_eq length_eq_length_filter_add
reduceOption_append 📖	—	—	—	—	—
reduceOption_concat 📖	—	—	—	—	reduceOption_cons_of_none reduceOption_cons_of_some reduceOption_append
reduceOption_concat_of_some 📖	—	—	—	—	reduceOption_append reduceOption_cons_of_some
reduceOption_cons_of_none 📖	—	—	—	—	—
reduceOption_cons_of_some 📖	—	—	—	—	—
reduceOption_eq_append_iff 📖	—	—	—	—	—
reduceOption_eq_concat_iff 📖	—	—	—	—	reduceOption_eq_append_iff reduceOption_eq_singleton_iff reduceOption_append reduceOption_replicate_none reduceOption_cons_of_some
reduceOption_eq_nil_iff 📖	—	—	—	—	—
reduceOption_eq_singleton_iff 📖	—	—	—	—	—
reduceOption_getElem?_iff 📖	—	—	—	—	reduceOption_mem_iff
reduceOption_length_eq 📖	—	—	—	—	reduceOption_cons_of_none reduceOption_cons_of_some
reduceOption_length_eq_iff 📖	—	—	—	—	reduceOption_length_eq
reduceOption_length_le 📖	—	—	—	—	length_eq_reduceOption_length_add_filter_none
reduceOption_length_lt_iff 📖	—	—	—	—	reduceOption_length_le reduceOption_length_eq_iff instIsEmptyFalse
reduceOption_map 📖	—	—	—	—	reduceOption_cons_of_none reduceOption_cons_of_some
reduceOption_mem_iff 📖	—	—	—	—	—
reduceOption_nil 📖	—	—	—	—	—
reduceOption_replicate_none 📖	—	—	—	—	—
reduceOption_singleton 📖	—	—	—	—	—

---

← Back to Index