mathlib documentation

data.list.func

def list.func.neg {α : Type u} [has_neg α] :
list αlist α

Equations
@[simp]
def list.func.set {α : Type u} [inhabited α] :
α → list αlist α

Equations
@[simp]
def list.func.get {α : Type u} [inhabited α] :
list α → α

Equations
def list.func.equiv {α : Type u} [inhabited α] :
list αlist α → Prop

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

Equations
def list.func.add {α : Type u} [has_zero α] [has_add α] :
list αlist αlist α

Equations
def list.func.sub {α : Type u} [has_zero α] [has_sub α] :
list αlist αlist α

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

@[simp]
theorem list.func.get_nil {α : Type u} [inhabited α] {k : } :

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

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

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

theorem list.func.mem_get_of_le {α : Type u} [inhabited α] {n : } {as : list α} :
n < as.lengthlist.func.get n as as

theorem list.func.mem_get_of_ne_zero {α : Type u} [inhabited α] {n : } {as : list α} :

theorem list.func.get_set_eq_of_ne {α : Type u} [inhabited α] {a : α} {as : list α} (k m : ) :
m klist.func.get m as {k a} = list.func.get m as

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

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

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

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

theorem list.func.equiv_symm {α : Type u} {as1 as2 : list α} [inhabited α] :
list.func.equiv as1 as2list.func.equiv as2 as1

theorem list.func.equiv_trans {α : Type u} {as1 as2 as3 : list α} [inhabited α] :
list.func.equiv as1 as2list.func.equiv as2 as3list.func.equiv as1 as3

theorem list.func.equiv_of_eq {α : Type u} {as1 as2 : list α} [inhabited α] :
as1 = as2list.func.equiv as1 as2

theorem list.func.eq_of_equiv {α : Type u} [inhabited α] {as1 as2 : list α} :
as1.length = as2.lengthlist.func.equiv as1 as2as1 = as2

@[simp]
theorem list.func.get_neg {α : Type u} [add_group α] {k : } {as : list α} :

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

theorem list.func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} (bs : list β) :

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

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 β) :

theorem list.func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} {as : list α} {bs : list β} :

@[simp]
theorem list.func.get_add {α : Type u} [add_monoid α] {k : } {xs ys : list α} :

@[simp]
theorem list.func.length_add {α : Type u} [has_zero α] [has_add α] {xs ys : list α} :

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

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

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

@[simp]
theorem list.func.get_sub {α : Type u} [add_group α] {k : } {xs ys : list α} :

@[simp]
theorem list.func.length_sub {α : Type u} [has_zero α] [has_sub α] {xs ys : list α} :

@[simp]
theorem list.func.nil_sub {α : Type} [add_group α] (as : list α) :

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