Documentation

Mathlib.Data.List.Infix

Prefixes, subfixes, infixes #

This file proves properties about

All those (except insert) are defined in Mathlib.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
ink
@[simp]
theorem List.prefix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁ <+: l₁ ++ l₂
source
ink
@[simp]
theorem List.suffix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₂ <:+ l₁ ++ l₂
source
ink
theorem List.infix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) :
l₂ <:+: l₁ ++ l₂ ++ l₃
source
ink
@[simp]
theorem List.infix_append' {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) :
l₂ <:+: l₁ ++ (l₂ ++ l₃)
source
ink
theorem List.isPrefix.isInfix {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ → l₁ <:+: l₂
source
ink
theorem List.isSuffix.isInfix {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ → l₁ <:+: l₂
source
ink
theorem List.nil_prefix {α : Type u_1} (l : List α) :
[] <+: l
source
ink
theorem List.nil_suffix {α : Type u_1} (l : List α) :
[] <:+ l
source
ink
theorem List.nil_infix {α : Type u_1} (l : List α) :
[] <:+: l
source
ink
theorem List.prefix_refl {α : Type u_1} (l : List α) :
l <+: l
source
ink
theorem List.suffix_refl {α : Type u_1} (l : List α) :
l <:+ l
source
ink
theorem List.infix_refl {α : Type u_1} (l : List α) :
l <:+: l
source
ink
theorem List.prefix_rfl {α : Type u_1} {l : List α} :
l <+: l
source
ink
theorem List.suffix_rfl {α : Type u_1} {l : List α} :
l <:+ l
source
ink
theorem List.infix_rfl {α : Type u_1} {l : List α} :
l <:+: l
source
ink
@[simp]
theorem List.suffix_cons {α : Type u_1} (a : α) (l : List α) :
l <:+ a :: l
source
ink
theorem List.prefix_concat {α : Type u_1} (a : α) (l : List α) :
l <+: List.concat l a
source
ink
theorem List.infix_cons {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} :
l₁ <:+: l₂ → l₁ <:+: a :: l₂
source
ink
theorem List.infix_concat {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} :
l₁ <:+: l₂ → l₁ <:+: List.concat l₂ a
source
ink
theorem List.isPrefix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
source
ink
theorem List.isSuffix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
source
ink
theorem List.isInfix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
source
ink
theorem List.isInfix.sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+: l₂ → List.Sublist l₁ l₂
source
ink
theorem List.isInfix.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁ <:+: l₂) :
l₁ ⊆ l₂
source
ink
theorem List.isPrefix.sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) :
List.Sublist l₁ l₂
source
ink
theorem List.isPrefix.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁ <+: l₂) :
l₁ ⊆ l₂
source
ink
theorem List.isSuffix.sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+ l₂) :
List.Sublist l₁ l₂
source
ink
theorem List.isSuffix.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁ <:+ l₂) :
l₁ ⊆ l₂
source
ink
@[simp]
theorem List.reverse_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} :
List.reverse l₁ <:+ List.reverse l₂ ↔ l₁ <+: l₂
source
ink
@[simp]
theorem List.reverse_prefix {α : Type u_1} {l₁ : List α} {l₂ : List α} :
List.reverse l₁ <+: List.reverse l₂ ↔ l₁ <:+ l₂
source
ink
@[simp]
theorem List.reverse_infix {α : Type u_1} {l₁ : List α} {l₂ : List α} :
List.reverse l₁ <:+: List.reverse l₂ ↔ l₁ <:+: l₂
source
ink
theorem List.isSuffix.reverse {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ → List.reverse l₁ <+: List.reverse l₂

Alias of the reverse direction of List.reverse_prefix.

source
ink
theorem List.isPrefix.reverse {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ → List.reverse l₁ <:+ List.reverse l₂

Alias of the reverse direction of List.reverse_suffix.

source
ink
theorem List.isInfix.reverse {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+: l₂ → List.reverse l₁ <:+: List.reverse l₂

Alias of the reverse direction of List.reverse_infix.

source
ink
theorem List.isInfix.length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+: l₂) :
List.length l₁ ≤ List.length l₂
source
ink
theorem List.isPrefix.length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) :
List.length l₁ ≤ List.length l₂
source
ink
theorem List.isSuffix.length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+ l₂) :
List.length l₁ ≤ List.length l₂
source
ink
theorem List.eq_nil_of_infix_nil {α : Type u_1} {l : List α} (h : l <:+: []) :
l = []
source
ink
@[simp]
theorem List.infix_nil_iff {α : Type u_1} {l : List α} :
l <:+: [] ↔ l = []
source
ink
@[simp]
theorem List.prefix_nil_iff {α : Type u_1} {l : List α} :
l <+: [] ↔ l = []
source
ink
@[simp]
theorem List.suffix_nil_iff {α : Type u_1} {l : List α} :
l <:+ [] ↔ l = []
source
ink
theorem List.eq_nil_of_prefix_nil {α : Type u_1} {l : List α} :
l <+: [] → l = []

Alias of the forward direction of List.prefix_nil_iff.

source
ink
theorem List.eq_nil_of_suffix_nil {α : Type u_1} {l : List α} :
l <:+ [] → l = []

Alias of the forward direction of List.suffix_nil_iff.

source
ink
theorem List.infix_iff_prefix_suffix {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂
source
ink
theorem List.eq_of_infix_of_length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+: l₂) :
List.length l₁ = List.length l₂ → l₁ = l₂
source
ink
theorem List.eq_of_prefix_of_length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) :
List.length l₁ = List.length l₂ → l₁ = l₂
source
ink
theorem List.eq_of_suffix_of_length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+ l₂) :
List.length l₁ = List.length l₂ → l₁ = l₂
source
ink
theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+: l₃ → l₂ <+: l₃ → List.length l₁ ≤ List.length l₂ → l₁ <+: l₂
source
ink
theorem List.prefix_or_prefix_of_prefix {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) :
l₁ <+: l₂ ∨ l₂ <+: l₁
source
ink
theorem List.suffix_of_suffix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : List.length l₁ ≤ List.length l₂) :
l₁ <:+ l₂
source
ink
theorem List.suffix_or_suffix_of_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) :
l₁ <:+ l₂ ∨ l₂ <:+ l₁
source
ink
theorem List.suffix_cons_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} :
l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
source
ink
theorem List.infix_cons_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} :
l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
source
ink
theorem List.infix_of_mem_join {α : Type u_1} {l : List α} {L : List (List α)} :
l ∈ L → l <:+: List.join L
source
ink
theorem List.prefix_append_right_inj {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) :
l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
source
ink
theorem List.prefix_cons_inj {α : Type u_1} {l₁ : List α} {l₂ : List α} (a : α) :
a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂
source
ink
theorem List.take_prefix {α : Type u_1} (n : ℕ) (l : List α) :
List.take n l <+: l
source
ink
theorem List.drop_suffix {α : Type u_1} (n : ℕ) (l : List α) :
List.drop n l <:+ l
source
ink
theorem List.take_sublist {α : Type u_1} (n : ℕ) (l : List α) :
List.Sublist (List.take n l) l
source
ink
theorem List.drop_sublist {α : Type u_1} (n : ℕ) (l : List α) :
List.Sublist (List.drop n l) l
source
ink
theorem List.take_subset {α : Type u_1} (n : ℕ) (l : List α) :
List.take n l ⊆ l
source
ink
theorem List.drop_subset {α : Type u_1} (n : ℕ) (l : List α) :
List.drop n l ⊆ l
source
ink
theorem List.mem_of_mem_take {α : Type u_1} {l : List α} {a : α} {n : ℕ} (h : a ∈ List.take n l) :
a ∈ l
source
ink
theorem List.dropSlice_sublist {α : Type u_1} (n : ℕ) (m : ℕ) (l : List α) :
List.Sublist (List.dropSlice n m l) l
source
ink
theorem List.dropSlice_subset {α : Type u_1} (n : ℕ) (m : ℕ) (l : List α) :
List.dropSlice n m l ⊆ l
source
ink
theorem List.mem_of_mem_dropSlice {α : Type u_1} {n : ℕ} {m : ℕ} {l : List α} {a : α} (h : a ∈ List.dropSlice n m l) :
a ∈ l
source
ink
theorem List.takeWhile_prefix {α : Type u_1} {l : List α} (p : α → Bool) :
List.takeWhile p l <+: l
source
ink
theorem List.dropWhile_suffix {α : Type u_1} {l : List α} (p : α → Bool) :
List.dropWhile p l <:+ l
source
ink
theorem List.dropLast_prefix {α : Type u_1} (l : List α) :
List.dropLast l <+: l
source
ink
theorem List.tail_suffix {α : Type u_1} (l : List α) :
List.tail l <:+ l
source
ink
theorem List.dropLast_sublist {α : Type u_1} (l : List α) :
List.Sublist (List.dropLast l) l
source
ink
theorem List.tail_sublist {α : Type u_1} (l : List α) :
List.Sublist (List.tail l) l
source
ink
theorem List.dropLast_subset {α : Type u_1} (l : List α) :
List.dropLast l ⊆ l
source
ink
theorem List.tail_subset {α : Type u_1} (l : List α) :
List.tail l ⊆ l
source
ink
theorem List.mem_of_mem_dropLast {α : Type u_1} {l : List α} {a : α} (h : a ∈ List.dropLast l) :
a ∈ l
source
ink
theorem List.mem_of_mem_tail {α : Type u_1} {l : List α} {a : α} (h : a ∈ List.tail l) :
a ∈ l
source
ink
theorem List.prefix_iff_eq_append {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ ↔ l₁ ++ List.drop (List.length l₁) l₂ = l₂
source
ink
theorem List.suffix_iff_eq_append {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ ↔ List.take (List.length l₂ - List.length l₁) l₂ ++ l₁ = l₂
source
ink
theorem List.prefix_iff_eq_take {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ ↔ l₁ = List.take (List.length l₁) l₂
source
ink
theorem List.suffix_iff_eq_drop {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ ↔ l₁ = List.drop (List.length l₂ - List.length l₁) l₂
source
ink
instance List.decidablePrefix {α : Type u_1} [inst : DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ <+: l₂)
Equations
source
ink
instance List.decidableSuffix {α : Type u_1} [inst : DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ <:+ l₂)
Equations
source
ink
instance List.decidableInfix {α : Type u_1} [inst : DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ <:+: l₂)
Equations
source
ink
theorem List.prefix_take_le_iff {α : Type u_1} {m : ℕ} {n : ℕ} {L : List (List (Option α))} (hm : m < List.length L) :
List.take m L <+: List.take n L ↔ m ≤ n
source
ink
theorem List.cons_prefix_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} {b : α} :
a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
source
ink
theorem List.isPrefix.map {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) (f : α → β) :
List.map f l₁ <+: List.map f l₂
source
ink
theorem List.isPrefix.filter_map {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) (f : α → Option β) :
List.filterMap f l₁ <+: List.filterMap f l₂
source
ink
theorem List.isPrefix.reduceOption {α : Type u_1} {l₁ : List (Option α)} {l₂ : List (Option α)} (h : l₁ <+: l₂) :
List.reduceOption l₁ <+: List.reduceOption l₂
source
ink
theorem List.isPrefix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <+: l₂) :
List.filter p l₁ <+: List.filter p l₂
source
ink
theorem List.isSuffix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+ l₂) :
List.filter p l₁ <:+ List.filter p l₂
source
ink
theorem List.isInfix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+: l₂) :
List.filter p l₁ <:+: List.filter p l₂
source
ink
instance List.instIsPartialOrderListIsPrefix {α : Type u_1} :
IsPartialOrder (List α) fun x x_1 => x <+: x_1
Equations
source
ink
instance List.instIsPartialOrderListIsSuffix {α : Type u_1} :
IsPartialOrder (List α) fun x x_1 => x <:+ x_1
Equations
source
ink
instance List.instIsPartialOrderListIsInfix {α : Type u_1} :
IsPartialOrder (List α) fun x x_1 => x <:+: x_1
Equations
source
ink
@[simp]
theorem List.mem_inits {α : Type u_1} (s : List α) (t : List α) :
s ∈ List.inits t ↔ s <+: t
source
ink
@[simp]
theorem List.mem_tails {α : Type u_1} (s : List α) (t : List α) :
s ∈ List.tails t ↔ s <:+ t
source
ink
theorem List.inits_cons {α : Type u_1} (a : α) (l : List α) :
List.inits (a :: l) = [] :: List.map (fun t => a :: t) (List.inits l)
source
ink
theorem List.tails_cons {α : Type u_1} (a : α) (l : List α) :
List.tails (a :: l) = (a :: l) :: List.tails l
source
ink
@[simp]
theorem List.inits_append {α : Type u_1} (s : List α) (t : List α) :
List.inits (s ++ t) = List.inits s ++ List.map (fun l => s ++ l) (List.tail (List.inits t))
source
ink
@[simp]
theorem List.tails_append {α : Type u_1} (s : List α) (t : List α) :
List.tails (s ++ t) = List.map (fun l => l ++ t) (List.tails s) ++ List.tail (List.tails t)
source
ink
theorem List.inits_eq_tails {α : Type u_1} (l : List α) :
List.inits l = List.reverse (List.map List.reverse (List.tails (List.reverse l)))
source
ink
theorem List.tails_eq_inits {α : Type u_1} (l : List α) :
List.tails l = List.reverse (List.map List.reverse (List.inits (List.reverse l)))
source
ink
theorem List.inits_reverse {α : Type u_1} (l : List α) :
List.inits (List.reverse l) = List.reverse (List.map List.reverse (List.tails l))
source
ink
theorem List.tails_reverse {α : Type u_1} (l : List α) :
List.tails (List.reverse l) = List.reverse (List.map List.reverse (List.inits l))
source
ink
theorem List.map_reverse_inits {α : Type u_1} (l : List α) :
List.map List.reverse (List.inits l) = List.reverse (List.tails (List.reverse l))
source
ink
theorem List.map_reverse_tails {α : Type u_1} (l : List α) :
List.map List.reverse (List.tails l) = List.reverse (List.inits (List.reverse l))
source
ink
@[simp]
theorem List.length_tails {α : Type u_1} (l : List α) :
List.length (List.tails l) = List.length l + 1
source
ink
@[simp]
theorem List.length_inits {α : Type u_1} (l : List α) :
List.length (List.inits l) = List.length l + 1
source
ink
@[simp]
theorem List.nth_le_tails {α : Type u_1} (l : List α) (n : ℕ) (hn : n < List.length (List.tails l)) :
List.nthLe (List.tails l) n hn = List.drop n l
source
ink
@[simp]
theorem List.nth_le_inits {α : Type u_1} (l : List α) (n : ℕ) (hn : n < List.length (List.inits l)) :
List.nthLe (List.inits l) n hn = List.take n l

insert #

source
ink
@[simp]
theorem List.insert_nil {α : Type u_1} [inst : DecidableEq α] (a : α) :
insert a [] = [a]
source
ink
theorem List.insert.def {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) :
insert a l = if a ∈ l then l else a :: l
source
ink
@[simp]
theorem List.suffix_insert {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) :
l <:+ List.insert a l
source
ink
theorem List.infix_insert {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) :
l <:+: List.insert a l
source
ink
theorem List.sublist_insert {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) :
List.Sublist l (List.insert a l)
source
ink
theorem List.subset_insert {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) :
l ⊆ List.insert a l
source
ink
theorem List.mem_of_mem_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} (hx : a ∈ l₁) (hl : l₁ <:+ l₂) :
a ∈ l₂