Prefixes, suffixes, infixes #
This file proves properties about
List.isPrefix
:l₁
is a prefix ofl₂
ifl₂
starts withl₁
.List.isSuffix
:l₁
is a suffix ofl₂
ifl₂
ends withl₁
.List.isInfix
:l₁
is an infix ofl₂
ifl₁
is a prefix of some suffix ofl₂
.List.inits
: The list of prefixes of a list.List.tails
: The list of prefixes of a list.insert
on lists
All those (except insert
) are defined in Mathlib.Data.List.Defs
.
Notation #
l₁ <+: l₂
:l₁
is a prefix ofl₂
.l₁ <:+ l₂
:l₁
is a suffix ofl₂
.l₁ <:+: l₂
:l₁
is an infix ofl₂
.
prefix, suffix, infix #
Alias of the reverse direction of List.reverse_prefix
.
Alias of the reverse direction of List.reverse_suffix
.
Alias of the reverse direction of List.reverse_infix
.
Alias of the forward direction of List.infix_nil
.
Alias of the forward direction of List.prefix_nil
.
Alias of the forward direction of List.suffix_nil
.
theorem
List.dropSlice_sublist
{α : Type u_1}
(n : ℕ)
(m : ℕ)
(l : List α)
:
(List.dropSlice n m l).Sublist l
theorem
List.mem_of_mem_dropSlice
{α : Type u_1}
{n : ℕ}
{m : ℕ}
{l : List α}
{a : α}
(h : a ∈ List.dropSlice n m l)
:
a ∈ l
theorem
List.IsPrefix.filterMap
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
(h : l₁ <+: l₂)
(f : α → Option β)
:
List.filterMap f l₁ <+: List.filterMap f l₂
@[deprecated List.IsPrefix.filterMap]
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₂
Alias of List.IsPrefix.filterMap
.
instance
List.instIsPartialOrderIsPrefix
{α : Type u_1}
:
IsPartialOrder (List α) fun (x x_1 : List α) => x <+: x_1
Equations
- ⋯ = ⋯
instance
List.instIsPartialOrderIsSuffix
{α : Type u_1}
:
IsPartialOrder (List α) fun (x x_1 : List α) => x <:+ x_1
Equations
- ⋯ = ⋯
instance
List.instIsPartialOrderIsInfix
{α : Type u_1}
:
IsPartialOrder (List α) fun (x x_1 : List α) => x <:+: x_1
Equations
- ⋯ = ⋯
insert #
@[simp]
theorem
List.suffix_insert
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
l <:+ List.insert a l
theorem
List.infix_insert
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
l <:+: List.insert a l
theorem
List.sublist_insert
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
l.Sublist (List.insert a l)