Commit 2023-01-05 23:05 9f4e5f90

View on Github →

feat: port Data.List.Infix (#1350)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Defs.lean

Created Mathlib/Data/List/Infix.lean

added theorem List.cons_prefix_iff

added theorem List.dropLast_prefix

added theorem List.dropLast_sublist

added theorem List.dropLast_subset

added theorem List.dropWhile_suffix

added theorem List.drop_sublist

added theorem List.drop_subset

added theorem List.drop_suffix

added theorem List.eq_nil_of_infix_nil

added theorem List.eq_of_infix_of_length_eq

added theorem List.eq_of_prefix_of_length_eq

added theorem List.eq_of_suffix_of_length_eq

added theorem List.infix_append'

added theorem List.infix_append

added theorem List.infix_concat

added theorem List.infix_cons

added theorem List.infix_cons_iff

added theorem List.infix_iff_prefix_suffix

added theorem List.infix_insert

added theorem List.infix_nil_iff

added theorem List.infix_of_mem_join

added theorem List.infix_refl

added theorem List.infix_rfl

added theorem List.inits_append

added theorem List.inits_cons

added theorem List.inits_eq_tails

added theorem List.inits_reverse

added theorem List.insert.def

added theorem List.insert_nil

added theorem List.isInfix.filter

added theorem List.isInfix.length_le

added theorem List.isInfix.trans

added theorem List.isPrefix.filter

added theorem List.isPrefix.filter_map

added theorem List.isPrefix.isInfix

added theorem List.isPrefix.length_le

added theorem List.isPrefix.map

added theorem List.isPrefix.reduceOption

added theorem List.isPrefix.trans

added theorem List.isSuffix.filter

added theorem List.isSuffix.isInfix

added theorem List.isSuffix.length_le

added theorem List.isSuffix.trans

added theorem List.length_inits

added theorem List.length_tails

added theorem List.map_reverse_inits

added theorem List.map_reverse_tails

added theorem List.mem_inits

added theorem List.mem_of_mem_dropLast

added theorem List.mem_of_mem_suffix

added theorem List.mem_of_mem_tail

added theorem List.mem_of_mem_take

added theorem List.mem_tails

added theorem List.nil_infix

added theorem List.nil_prefix

added theorem List.nil_suffix

added theorem List.nth_le_inits

added theorem List.nth_le_tails

added theorem List.prefix_append

added theorem List.prefix_append_right_inj

added theorem List.prefix_concat

added theorem List.prefix_cons_inj

added theorem List.prefix_iff_eq_append

added theorem List.prefix_iff_eq_take

added theorem List.prefix_nil_iff

added theorem List.prefix_of_prefix_length_le

added theorem List.prefix_or_prefix_of_prefix

added theorem List.prefix_refl

added theorem List.prefix_rfl

added theorem List.prefix_take_le_iff

added theorem List.reverse_infix

added theorem List.reverse_prefix

added theorem List.reverse_suffix

added theorem List.sublist_insert

added theorem List.subset_insert

added theorem List.suffix_append

added theorem List.suffix_cons

added theorem List.suffix_cons_iff

added theorem List.suffix_iff_eq_append

added theorem List.suffix_iff_eq_drop

added theorem List.suffix_insert

added theorem List.suffix_nil_iff

added theorem List.suffix_of_suffix_length_le

added theorem List.suffix_or_suffix_of_suffix

added theorem List.suffix_refl

added theorem List.suffix_rfl

added theorem List.tail_sublist

added theorem List.tail_subset

added theorem List.tail_suffix

added theorem List.tails_append

added theorem List.tails_cons

added theorem List.tails_eq_inits

added theorem List.tails_reverse

added theorem List.takeWhile_prefix

added theorem List.take_prefix

added theorem List.take_sublist

added theorem List.take_subset