Equations
- list.func.neg as = list.map (λ (a : α), -a) as
@[simp]
Equations
- list.func.set a (h :: as) (k + 1) = h :: list.func.set a as k
- list.func.set a (_x :: as) 0 = a :: as
- list.func.set a list.nil (k + 1) = inhabited.default α :: list.func.set a list.nil k
- list.func.set a list.nil 0 = [a]
@[simp]
Equations
- list.func.get (n + 1) (a :: as) = list.func.get n as
- list.func.get n.succ list.nil = inhabited.default α
- list.func.get 0 (a :: as) = a
- list.func.get 0 list.nil = inhabited.default α
Equations
- list.func.equiv as1 as2 = ∀ (m : ℕ), list.func.get m as1 = list.func.get m as2
@[simp]
Equations
- list.func.pointwise f (a :: as) (b :: bs) = f a b :: list.func.pointwise f as bs
- list.func.pointwise f (a :: as) list.nil = list.map (λ (x : α), f x (inhabited.default β)) (a :: as)
- list.func.pointwise f list.nil (b :: bs) = list.map (f (inhabited.default α)) (b :: bs)
- list.func.pointwise f list.nil list.nil = list.nil
Equations
Equations
@[simp]
theorem
list.func.get_eq_default_of_le
{α : Type u}
[inhabited α]
(k : ℕ)
{as : list α} :
as.length ≤ k → list.func.get k as = inhabited.default α
@[simp]
theorem
list.func.get_set
{α : Type u}
[inhabited α]
{a : α}
{k : ℕ}
{as : list α} :
list.func.get k (list.func.set a as k) = 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.length → list.func.get n as ∈ as
theorem
list.func.mem_get_of_ne_zero
{α : Type u}
[inhabited α]
{n : ℕ}
{as : list α} :
list.func.get n as ≠ inhabited.default α → list.func.get n as ∈ as
theorem
list.func.get_set_eq_of_ne
{α : Type u}
[inhabited α]
{a : α}
{as : list α}
(k m : ℕ) :
m ≠ k → list.func.get m (list.func.set a as k) = list.func.get m as
theorem
list.func.get_map
{α : Type u}
{β : Type v}
[inhabited α]
[inhabited β]
{f : α → β}
{n : ℕ}
{as : list α} :
n < as.length → list.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 (inhabited.default α) = inhabited.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 (inhabited.default α))
(a_1 : ∀ (x : α), x ∈ as → p x)
(n : ℕ) :
p (list.func.get n as)
theorem
list.func.equiv_symm
{α : Type u}
{as1 as2 : list α}
[inhabited α] :
list.func.equiv as1 as2 → list.func.equiv as2 as1
theorem
list.func.equiv_trans
{α : Type u}
{as1 as2 as3 : list α}
[inhabited α] :
list.func.equiv as1 as2 → list.func.equiv as2 as3 → list.func.equiv as1 as3
theorem
list.func.equiv_of_eq
{α : Type u}
{as1 as2 : list α}
[inhabited α] :
as1 = as2 → list.func.equiv as1 as2
theorem
list.func.eq_of_equiv
{α : Type u}
[inhabited α]
{as1 as2 : list α} :
as1.length = as2.length → list.func.equiv as1 as2 → as1 = as2
@[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
@[simp]
theorem
list.func.length_neg
{α : Type u}
[has_neg α]
(as : list α) :
(list.func.neg as).length = as.length
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 (inhabited.default α)) bs
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 (inhabited.default β)) as
theorem
list.func.get_pointwise
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
[inhabited γ]
{f : α → β → γ}
(h1 : f (inhabited.default α) (inhabited.default β) = inhabited.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)
@[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
@[simp]
theorem
list.func.nil_add
{α : Type u}
[add_monoid α]
(as : list α) :
list.func.add list.nil as = as
@[simp]
theorem
list.func.add_nil
{α : Type u}
[add_monoid α]
(as : list α) :
list.func.add as list.nil = as
@[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
@[simp]
theorem
list.func.nil_sub
{α : Type}
[add_group α]
(as : list α) :
list.func.sub list.nil as = list.func.neg as
@[simp]