mathlib3 documentation

data.list.infix

Prefixes, subfixes, infixes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves properties about

All those (except insert) are defined in data.list.defs.

Notation #

l₁ <+: l₂: l₁ is a prefix of l₂. l₁ <:+ l₂: l₁ is a subfix of l₂. l₁ <:+: l₂: l₁ is an infix of l₂.

prefix, suffix, infix #

source
@[simp]
theorem list.prefix_append {α : Type u_1} (l₁ l₂ : list α) :
l₁ <+: l₁ ++ l₂
source
@[simp]
theorem list.suffix_append {α : Type u_1} (l₁ l₂ : list α) :
l₂ <:+ l₁ ++ l₂
source
theorem list.infix_append {α : Type u_1} (l₁ l₂ l₃ : list α) :
l₂ <:+: l₁ ++ l₂ ++ l₃
source
@[simp]
theorem list.infix_append' {α : Type u_1} (l₁ l₂ l₃ : list α) :
l₂ <:+: l₁ ++ (l₂ ++ l₃)
source
theorem list.is_prefix.is_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ → l₁ <:+: l₂
source
theorem list.is_suffix.is_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ → l₁ <:+: l₂
source
theorem list.nil_prefix {α : Type u_1} (l : list α) :
list.nil <+: l
source
theorem list.nil_suffix {α : Type u_1} (l : list α) :
list.nil <:+ l
source
theorem list.nil_infix {α : Type u_1} (l : list α) :
list.nil <:+: l
source
@[refl]
theorem list.prefix_refl {α : Type u_1} (l : list α) :
l <+: l
source
@[refl]
theorem list.suffix_refl {α : Type u_1} (l : list α) :
l <:+ l
source
@[refl]
theorem list.infix_refl {α : Type u_1} (l : list α) :
l <:+: l
source
theorem list.prefix_rfl {α : Type u_1} {l : list α} :
l <+: l
source
theorem list.suffix_rfl {α : Type u_1} {l : list α} :
l <:+ l
source
theorem list.infix_rfl {α : Type u_1} {l : list α} :
l <:+: l
source
@[simp]
theorem list.suffix_cons {α : Type u_1} (a : α) (l : list α) :
l <:+ a :: l
source
theorem list.prefix_concat {α : Type u_1} (a : α) (l : list α) :
l <+: l.concat a
source
theorem list.infix_cons {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: l₂ → l₁ <:+: a :: l₂
source
theorem list.infix_concat {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: l₂ → l₁ <:+: l₂.concat a
source
@[trans]
theorem list.is_prefix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
source
@[trans]
theorem list.is_suffix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
source
@[trans]
theorem list.is_infix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
source
@[protected]
theorem list.is_infix.sublist {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+: l₂ → l₁ <+ l₂
source
@[protected]
theorem list.is_infix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <:+: l₂) :
l₁ ⊆ l₂
source
@[protected]
theorem list.is_prefix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁ <+ l₂
source
@[protected]
theorem list.is_prefix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <+: l₂) :
l₁ ⊆ l₂
source
@[protected]
theorem list.is_suffix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁ <+ l₂
source
@[protected]
theorem list.is_suffix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <:+ l₂) :
l₁ ⊆ l₂
source
@[simp]
theorem list.reverse_suffix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂
source
@[simp]
theorem list.reverse_prefix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂
source
@[simp]
theorem list.reverse_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂
source
theorem list.is_suffix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ → l₁.reverse <+: l₂.reverse

Alias of the reverse direction of list.reverse_prefix.

source
theorem list.is_prefix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ → l₁.reverse <:+ l₂.reverse

Alias of the reverse direction of list.reverse_suffix.

source
theorem list.is_infix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+: l₂ → l₁.reverse <:+: l₂.reverse

Alias of the reverse direction of list.reverse_infix.

source
theorem list.is_infix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+: l₂) :
l₁.length ≤ l₂.length
source
theorem list.is_prefix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁.length ≤ l₂.length
source
theorem list.is_suffix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁.length ≤ l₂.length
source
theorem list.eq_nil_of_infix_nil {α : Type u_1} {l : list α} (h : l <:+: list.nil) :
l = list.nil
source
@[simp]
theorem list.infix_nil_iff {α : Type u_1} {l : list α} :
l <:+: list.nil ↔ l = list.nil
source
@[simp]
theorem list.prefix_nil_iff {α : Type u_1} {l : list α} :
l <+: list.nil ↔ l = list.nil
source
@[simp]
theorem list.suffix_nil_iff {α : Type u_1} {l : list α} :
l <:+ list.nil ↔ l = list.nil
source
theorem list.eq_nil_of_prefix_nil {α : Type u_1} {l : list α} :
l <+: list.nil → l = list.nil

Alias of the forward direction of list.prefix_nil_iff.

source
theorem list.eq_nil_of_suffix_nil {α : Type u_1} {l : list α} :
l <:+ list.nil → l = list.nil

Alias of the forward direction of list.suffix_nil_iff.

source
theorem list.infix_iff_prefix_suffix {α : Type u_1} (l₁ l₂ : list α) :
l₁ <:+: l₂ ↔ ∃ (t : list α), l₁ <+: t ∧ t <:+ l₂
source
theorem list.eq_of_infix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+: l₂) :
l₁.length = l₂.length → l₁ = l₂
source
theorem list.eq_of_prefix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁.length = l₂.length → l₁ = l₂
source
theorem list.eq_of_suffix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁.length = l₂.length → l₁ = l₂
source
theorem list.prefix_of_prefix_length_le {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → l₁ <+: l₂
source
theorem list.prefix_or_prefix_of_prefix {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) :
l₁ <+: l₂ ∨ l₂ <+: l₁
source
theorem list.suffix_of_suffix_length_le {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : l₁.length ≤ l₂.length) :
l₁ <:+ l₂
source
theorem list.suffix_or_suffix_of_suffix {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) :
l₁ <:+ l₂ ∨ l₂ <:+ l₁
source
theorem list.suffix_cons_iff {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
source
theorem list.infix_cons_iff {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
source
theorem list.infix_of_mem_join {α : Type u_1} {l : list α} {L : list (list α)} :
l ∈ L → l <:+: L.join
source
theorem list.prefix_append_right_inj {α : Type u_1} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
source
theorem list.prefix_cons_inj {α : Type u_1} {l₁ l₂ : list α} (a : α) :
a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂
source
theorem list.take_prefix {α : Type u_1} (n : ℕ) (l : list α) :
list.take n l <+: l
source
theorem list.drop_suffix {α : Type u_1} (n : ℕ) (l : list α) :
list.drop n l <:+ l
source
theorem list.take_sublist {α : Type u_1} (n : ℕ) (l : list α) :
list.take n l <+ l
source
theorem list.drop_sublist {α : Type u_1} (n : ℕ) (l : list α) :
list.drop n l <+ l
source
theorem list.take_subset {α : Type u_1} (n : ℕ) (l : list α) :
list.take n l ⊆ l
source
theorem list.drop_subset {α : Type u_1} (n : ℕ) (l : list α) :
list.drop n l ⊆ l
source
theorem list.mem_of_mem_take {α : Type u_1} {l : list α} {a : α} {n : ℕ} (h : a ∈ list.take n l) :
a ∈ l
source
theorem list.mem_of_mem_drop {α : Type u_1} {l : list α} {a : α} {n : ℕ} (h : a ∈ list.drop n l) :
a ∈ l
source
theorem list.slice_sublist {α : Type u_1} (n m : ℕ) (l : list α) :
list.slice n m l <+ l
source
theorem list.slice_subset {α : Type u_1} (n m : ℕ) (l : list α) :
list.slice n m l ⊆ l
source
theorem list.mem_of_mem_slice {α : Type u_1} {n m : ℕ} {l : list α} {a : α} (h : a ∈ list.slice n m l) :
a ∈ l
source
theorem list.take_while_prefix {α : Type u_1} {l : list α} (p : α → Prop) [decidable_pred p] :
list.take_while p l <+: l
source
theorem list.drop_while_suffix {α : Type u_1} {l : list α} (p : α → Prop) [decidable_pred p] :
list.drop_while p l <:+ l
source
theorem list.init_prefix {α : Type u_1} (l : list α) :
l.init <+: l
source
theorem list.tail_suffix {α : Type u_1} (l : list α) :
l.tail <:+ l
source
theorem list.init_sublist {α : Type u_1} (l : list α) :
l.init <+ l
source
theorem list.tail_sublist {α : Type u_1} (l : list α) :
l.tail <+ l
source
theorem list.init_subset {α : Type u_1} (l : list α) :
l.init ⊆ l
source
theorem list.tail_subset {α : Type u_1} (l : list α) :
l.tail ⊆ l
source
theorem list.mem_of_mem_init {α : Type u_1} {l : list α} {a : α} (h : a ∈ l.init) :
a ∈ l
source
theorem list.mem_of_mem_tail {α : Type u_1} {l : list α} {a : α} (h : a ∈ l.tail) :
a ∈ l
source
theorem list.prefix_iff_eq_append {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ ↔ l₁ ++ list.drop l₁.length l₂ = l₂
source
theorem list.suffix_iff_eq_append {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ ↔ list.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
source
theorem list.prefix_iff_eq_take {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ ↔ l₁ = list.take l₁.length l₂
source
theorem list.suffix_iff_eq_drop {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ ↔ l₁ = list.drop (l₂.length - l₁.length) l₂
source
@[protected, instance]
def list.decidable_prefix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <+: l₂)
Equations
source
@[protected, instance]
def list.decidable_suffix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <:+ l₂)
Equations
source
@[protected, instance]
def list.decidable_infix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <:+: l₂)
Equations
source
theorem list.prefix_take_le_iff {α : Type u_1} {m n : ℕ} {L : list (list (option α))} (hm : m < L.length) :
list.take m L <+: list.take n L ↔ m ≤ n
source
theorem list.cons_prefix_iff {α : Type u_1} {l₁ l₂ : list α} {a b : α} :
a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
source
theorem list.is_prefix.map {α : Type u_1} {β : Type u_2} {l₁ l₂ : list α} (h : l₁ <+: l₂) (f : α → β) :
list.map f l₁ <+: list.map f l₂
source
theorem list.is_prefix.filter_map {α : Type u_1} {β : Type u_2} {l₁ l₂ : list α} (h : l₁ <+: l₂) (f : α → option β) :
list.filter_map f l₁ <+: list.filter_map f l₂
source
theorem list.is_prefix.reduce_option {α : Type u_1} {l₁ l₂ : list (option α)} (h : l₁ <+: l₂) :
l₁.reduce_option <+: l₂.reduce_option
source
theorem list.is_prefix.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <+: l₂) :
list.filter p l₁ <+: list.filter p l₂
source
theorem list.is_suffix.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <:+ l₂) :
list.filter p l₁ <:+ list.filter p l₂
source
theorem list.is_infix.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <:+: l₂) :
list.filter p l₁ <:+: list.filter p l₂
source
@[protected, instance]
def list.is_prefix.is_partial_order {α : Type u_1} :
is_partial_order (list α) list.is_prefix
source
@[protected, instance]
def list.is_suffix.is_partial_order {α : Type u_1} :
is_partial_order (list α) list.is_suffix
source
@[protected, instance]
def list.is_infix.is_partial_order {α : Type u_1} :
is_partial_order (list α) list.is_infix
source
@[simp]
theorem list.mem_inits {α : Type u_1} (s t : list α) :
s ∈ t.inits ↔ s <+: t
source
@[simp]
theorem list.mem_tails {α : Type u_1} (s t : list α) :
s ∈ t.tails ↔ s <:+ t
source
theorem list.inits_cons {α : Type u_1} (a : α) (l : list α) :
(a :: l).inits = list.nil :: list.map (λ (t : list α), a :: t) l.inits
source
theorem list.tails_cons {α : Type u_1} (a : α) (l : list α) :
(a :: l).tails = (a :: l) :: l.tails
source
@[simp]
theorem list.inits_append {α : Type u_1} (s t : list α) :
(s ++ t).inits = s.inits ++ list.map (λ (l : list α), s ++ l) t.inits.tail
source
@[simp]
theorem list.tails_append {α : Type u_1} (s t : list α) :
(s ++ t).tails = list.map (λ (l : list α), l ++ t) s.tails ++ t.tails.tail
source
theorem list.inits_eq_tails {α : Type u_1} (l : list α) :
l.inits = (list.map list.reverse l.reverse.tails).reverse
source
theorem list.tails_eq_inits {α : Type u_1} (l : list α) :
l.tails = (list.map list.reverse l.reverse.inits).reverse
source
theorem list.inits_reverse {α : Type u_1} (l : list α) :
l.reverse.inits = (list.map list.reverse l.tails).reverse
source
theorem list.tails_reverse {α : Type u_1} (l : list α) :
l.reverse.tails = (list.map list.reverse l.inits).reverse
source
theorem list.map_reverse_inits {α : Type u_1} (l : list α) :
list.map list.reverse l.inits = l.reverse.tails.reverse
source
theorem list.map_reverse_tails {α : Type u_1} (l : list α) :
list.map list.reverse l.tails = l.reverse.inits.reverse
source
@[simp]
theorem list.length_tails {α : Type u_1} (l : list α) :
l.tails.length = l.length + 1
source
@[simp]
theorem list.length_inits {α : Type u_1} (l : list α) :
l.inits.length = l.length + 1
source
@[simp]
theorem list.nth_le_tails {α : Type u_1} (l : list α) (n : ℕ) (hn : n < l.tails.length) :
l.tails.nth_le n hn = list.drop n l
source
@[simp]
theorem list.nth_le_inits {α : Type u_1} (l : list α) (n : ℕ) (hn : n < l.inits.length) :
l.inits.nth_le n hn = list.take n l

insert #

source
@[simp]
theorem list.insert_nil {α : Type u_1} [decidable_eq α] (a : α) :
has_insert.insert a list.nil = [a]
source
theorem list.insert.def {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
has_insert.insert a l = ite (a ∈ l) l (a :: l)
source
@[simp]
theorem list.insert_of_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a ∈ l) :
has_insert.insert a l = l
source
@[simp]
theorem list.insert_of_not_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a ∉ l) :
has_insert.insert a l = a :: l
source
@[simp]
theorem list.mem_insert_iff {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] :
a ∈ has_insert.insert b l ↔ a = b ∨ a ∈ l
source
@[simp]
theorem list.suffix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l <:+ has_insert.insert a l
source
theorem list.infix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l <:+: has_insert.insert a l
source
theorem list.sublist_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l <+ list.insert a l
source
theorem list.subset_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l ⊆ list.insert a l
source
@[simp]
theorem list.mem_insert_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
a ∈ list.insert a l
source
theorem list.mem_insert_of_mem {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] (h : a ∈ l) :
a ∈ has_insert.insert b l
source
theorem list.eq_or_mem_of_mem_insert {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] (h : a ∈ has_insert.insert b l) :
a = b ∨ a ∈ l
source
@[simp]
theorem list.length_insert_of_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a ∈ l) :
(has_insert.insert a l).length = l.length
source
@[simp]
theorem list.length_insert_of_not_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a ∉ l) :
(has_insert.insert a l).length = l.length + 1
source
theorem list.mem_of_mem_suffix {α : Type u_1} {l₁ l₂ : list α} {a : α} (hx : a ∈ l₁) (hl : l₁ <:+ l₂) :
a ∈ l₂