mathlib documentation

data.list.func

source
def list.func.neg {α : Type u} [has_neg α] (as : list α) :
list α

Equations
source
@[simp]
def list.func.set {α : Type u} [inhabited α] (a : α) (a_1 : list α) (a_2 : ℕ) :
list α

Equations
source
@[simp]
def list.func.get {α : Type u} [inhabited α] (a : ℕ) (a_1 : list α) :
α

Equations
source
def list.func.equiv {α : Type u} [inhabited α] (as1 as2 : list α) :
Prop

Equations
source
@[simp]
def list.func.pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] (f : α → β → γ) (a : list α) (a_1 : list β) :
list γ

Equations
source
def list.func.add {α : Type u} [has_zero α] [has_add α] (a a_1 : list α) :
list α

Equations
source
def list.func.sub {α : Type u} [has_zero α] [has_sub α] (a a_1 : list α) :
list α

Equations
source
theorem list.func.length_set {α : Type u} {a : α} [inhabited α] {m : ℕ} {as : list α} :
as {m ↦ a}.length = max as.length (m + 1)

source
@[simp]
theorem list.func.get_nil {α : Type u} [inhabited α] {k : ℕ} :
list.func.get k list.nil = default α

source
theorem list.func.get_eq_default_of_le {α : Type u} [inhabited α] (k : ℕ) {as : list α} (a : as.length ≤ k) :
list.func.get k as = default α

source
@[simp]
theorem list.func.get_set {α : Type u} [inhabited α] {a : α} {k : ℕ} {as : list α} :
list.func.get k as {k ↦ a} = a

source
theorem list.func.eq_get_of_mem {α : Type u} [inhabited α] {a : α} {as : list α} (a_1 : a ∈ as) :
∃ (n : ℕ), α → a = list.func.get n as

source
theorem list.func.mem_get_of_le {α : Type u} [inhabited α] {n : ℕ} {as : list α} (a : n < as.length) :
list.func.get n as ∈ as

source
theorem list.func.mem_get_of_ne_zero {α : Type u} [inhabited α] {n : ℕ} {as : list α} (a : list.func.get n as ≠ default α) :
list.func.get n as ∈ as

source
theorem list.func.get_set_eq_of_ne {α : Type u} [inhabited α] {a : α} {as : list α} (k m : ℕ) (a_1 : m ≠ k) :
list.func.get m as {k ↦ a} = list.func.get m as

source
theorem list.func.get_map {α : Type u} {β : Type v} [inhabited α] [inhabited β] {f : α → β} {n : ℕ} {as : list α} (a : n < as.length) :
list.func.get n (list.map f as) = f (list.func.get n as)

source
theorem list.func.get_map' {α : Type u} {β : Type v} [inhabited α] [inhabited β] {f : α → β} {n : ℕ} {as : list α} (a : f (default α) = default β) :
list.func.get n (list.map f as) = f (list.func.get n as)

source
theorem list.func.forall_val_of_forall_mem {α : Type u} [inhabited α] {as : list α} {p : α → Prop} (a : p (default α)) (a_1 : ∀ (x : α), x ∈ as → p x) (n : ℕ) :
p (list.func.get n as)

source
theorem list.func.equiv_refl {α : Type u} {as : list α} [inhabited α] :
list.func.equiv as as

source
theorem list.func.equiv_symm {α : Type u} {as1 as2 : list α} [inhabited α] (a : list.func.equiv as1 as2) :
list.func.equiv as2 as1

source
theorem list.func.equiv_trans {α : Type u} {as1 as2 as3 : list α} [inhabited α] (a : list.func.equiv as1 as2) (a_1 : list.func.equiv as2 as3) :
list.func.equiv as1 as3

source
theorem list.func.equiv_of_eq {α : Type u} {as1 as2 : list α} [inhabited α] (a : as1 = as2) :
list.func.equiv as1 as2

source
theorem list.func.eq_of_equiv {α : Type u} [inhabited α] {as1 as2 : list α} (a : as1.length = as2.length) (a_1 : list.func.equiv as1 as2) :
as1 = as2

source
@[simp]
theorem list.func.get_neg {α : Type u} [add_group α] {k : ℕ} {as : list α} :
list.func.get k (list.func.neg as) = -list.func.get k as

source
@[simp]
theorem list.func.length_neg {α : Type u} [has_neg α] (as : list α) :
(list.func.neg as).length = as.length

source
theorem list.func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} (bs : list β) :
list.func.pointwise f list.nil bs = list.map (f (default α)) bs

source
theorem list.func.pointwise_nil {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} (as : list α) :
list.func.pointwise f as list.nil = list.map (λ (a : α), f a (default β)) as

source
theorem list.func.get_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] [inhabited γ] {f : α → β → γ} (h1 : f (default α) (default β) = default γ) (k : ℕ) (as : list α) (bs : list β) :
list.func.get k (list.func.pointwise f as bs) = f (list.func.get k as) (list.func.get k bs)

source
theorem list.func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} {as : list α} {bs : list β} :
(list.func.pointwise f as bs).length = max as.length bs.length

source
@[simp]
theorem list.func.get_add {α : Type u} [add_monoid α] {k : ℕ} {xs ys : list α} :
list.func.get k (list.func.add xs ys) = list.func.get k xs + list.func.get k ys

source
@[simp]
theorem list.func.length_add {α : Type u} [has_zero α] [has_add α] {xs ys : list α} :
(list.func.add xs ys).length = max xs.length ys.length

source
@[simp]
theorem list.func.nil_add {α : Type u} [add_monoid α] (as : list α) :
list.func.add list.nil as = as

source
@[simp]
theorem list.func.add_nil {α : Type u} [add_monoid α] (as : list α) :
list.func.add as list.nil = as

source
theorem list.func.map_add_map {α : Type u} [add_monoid α] (f g : α → α) {as : list α} :
list.func.add (list.map f as) (list.map g as) = list.map (λ (x : α), f x + g x) as

source
@[simp]
theorem list.func.get_sub {α : Type u} [add_group α] {k : ℕ} {xs ys : list α} :
list.func.get k (list.func.sub xs ys) = list.func.get k xs - list.func.get k ys

source
@[simp]
theorem list.func.length_sub {α : Type u} [has_zero α] [has_sub α] {xs ys : list α} :
(list.func.sub xs ys).length = max xs.length ys.length

source
@[simp]
theorem list.func.nil_sub {α : Type} [add_group α] (as : list α) :
list.func.sub list.nil as = list.func.neg as

source
@[simp]
theorem list.func.sub_nil {α : Type} [add_group α] (as : list α) :
list.func.sub as list.nil = as