Documentation Verification Report

Infix

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

Statistics

MetricCount
DefinitionsdecidableInfix
1
TheoremsflatMap, flatten, nodup, drop, flatMap, flatten, nodup, reduceOption, take, flatMap, flatten, nodup, concat_get_prefix, dropSlice_sublist, dropSlice_subset, getElem_inits, getElem_tails, get_inits, get_tails, infix_antisymm, infix_insert, infix_singleton_iff, inits_append, inits_cons, inits_eq_tails, inits_reverse, insert_eq_ite, instIsPartialOrderIsInfix, instIsPartialOrderIsPrefix, instIsPartialOrderIsSuffix, isPrefix_append_of_length, length_inits, length_tails, map_inits, map_reverse_inits, map_reverse_tails, map_tails, mem_inits, mem_of_mem_dropLast, mem_of_mem_dropSlice, mem_tails, prefix_append_drop, singleton_infix_iff, singleton_infix_singleton_iff, sublist_insert, subset_insert, suffix_insert, tail_subset, tails_append, tails_cons, tails_eq_inits, tails_reverse, take_inits, take_isPrefix_take
54
Total55

List

Definitions

NameCategoryTheorems
decidableInfix 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
concat_get_prefix 📖
dropSlice_sublist 📖dropSlice_eq
dropSlice_subset 📖dropSlice_sublist
getElem_inits 📖
getElem_tails 📖
get_inits 📖getElem_inits
get_tails 📖getElem_tails
infix_antisymm 📖Sublist.antisymm
infix_insert 📖suffix_insert
infix_singleton_iff 📖instIsEmptyFalse
inits_append 📖
inits_cons 📖
inits_eq_tails 📖tails_append
inits_reverse 📖tails_eq_inits
Function.Involutive.comp_self
insert_eq_ite 📖mathematicalinstInsertOfDecidableEq_mathlib
instIsPartialOrderIsInfix 📖mathematicalIsPartialOrderLE.le.antisymm
instIsPartialOrderIsPrefix 📖mathematicalIsPartialOrderLE.le.antisymm
instIsPartialOrderIsSuffix 📖mathematicalIsPartialOrderLE.le.antisymm
isPrefix_append_of_length 📖take_eq_left_iff
length_inits 📖inits_eq_tails
length_tails
length_tails 📖
map_inits 📖inits_append
map_reverse_inits 📖inits_eq_tails
Function.Involutive.comp_self
map_reverse_tails 📖tails_eq_inits
Function.Involutive.comp_self
map_tails 📖tails_append
mem_inits 📖
mem_of_mem_dropLast 📖
mem_of_mem_dropSlice 📖dropSlice_subset
mem_tails 📖
prefix_append_drop 📖
singleton_infix_iff 📖
singleton_infix_singleton_iff 📖
sublist_insert 📖suffix_insert
subset_insert 📖sublist_insert
suffix_insert 📖
tail_subset 📖
tails_append 📖
tails_cons 📖
tails_eq_inits 📖inits_append
tails_reverse 📖inits_eq_tails
Function.Involutive.comp_self
take_inits 📖length_inits
getElem_inits
take_isPrefix_take 📖

List.IsInfix

Theorems

NameKindAssumesProvesValidatesDepends On
flatMap 📖flatten
flatten 📖
nodup 📖

List.IsPrefix

Theorems

NameKindAssumesProvesValidatesDepends On
drop 📖
flatMap 📖flatten
flatten 📖
nodup 📖
reduceOption 📖
take 📖

List.IsSuffix

Theorems

NameKindAssumesProvesValidatesDepends On
flatMap 📖flatten
flatten 📖
nodup 📖

---

← Back to Index