mem #
@[simp]
drop #
zipWith #
theorem
List.zipWith_distrib_tail :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1},
(List.zipWith f l l').tail = List.zipWith f l.tail l'.tail
List subset #
instance
List.instTransMemSubset_batteries
{α : Type u_1}
:
Trans Membership.mem Subset Membership.mem
Equations
- List.instTransMemSubset_batteries = { trans := ⋯ }
Equations
- List.instTransSubset_batteries = { trans := ⋯ }
sublists #
Equations
- List.instTransSublist = { trans := ⋯ }
@[simp]
Equations
- List.instTransSublistSubset = { trans := ⋯ }
Equations
- List.instTransSubsetSublist = { trans := ⋯ }
Equations
- List.instTransMemSublist = { trans := ⋯ }
@[simp]
theorem
List.replicate_sublist_replicate
{α : Type u_1}
{m : Nat}
{n : Nat}
(a : α)
:
(List.replicate m a).Sublist (List.replicate n a) ↔ m ≤ n
instance
List.instDecidableSublistOfDecidableEq
{α : Type u_1}
[DecidableEq α]
(l₁ : List α)
(l₂ : List α)
:
Decidable (l₁.Sublist l₂)
Equations
- l₁.instDecidableSublistOfDecidableEq l₂ = decidable_of_iff (l₁.isSublist l₂ = true) ⋯
tail #
next? #
get? #
drop #
modifyNth #
@[simp]
@[simp]
theorem
List.modifyNth_zero_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
:
List.modifyNth f 0 (a :: l) = f a :: l
@[simp]
theorem
List.modifyNth_succ_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
(n : Nat)
:
List.modifyNth f (n + 1) (a :: l) = a :: List.modifyNth f n l
theorem
List.eraseIdx_eq_modifyNthTail
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyNthTail List.tail n l
@[deprecated List.eraseIdx_eq_modifyNthTail]
theorem
List.removeNth_eq_nth_tail
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyNthTail List.tail n l
Alias of List.eraseIdx_eq_modifyNthTail
.
theorem
List.getElem?_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modifyNth f n l)[m]? = (fun (a : α) => if n = m then f a else a) <$> l[m]?
@[deprecated List.getElem?_modifyNth]
theorem
List.get?_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modifyNth f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m
theorem
List.modifyNthTail_add
{α : Type u_1}
(f : List α → List α)
(n : Nat)
(l₁ : List α)
(l₂ : List α)
:
List.modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂
@[simp]
theorem
List.modify_get?_length
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l).length = l.length
@[simp]
theorem
List.getElem?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l)[n]? = f <$> l[n]?
@[deprecated List.getElem?_modifyNth_eq]
theorem
List.get?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l).get? n = f <$> l.get? n
@[simp]
theorem
List.getElem?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modifyNth f m l)[n]? = l[n]?
@[deprecated List.getElem?_modifyNth_ne]
theorem
List.get?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modifyNth f m l).get? n = l.get? n
theorem
List.modifyNth_eq_take_drop
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modifyNth f n l = List.take n l ++ List.modifyHead f (List.drop n l)
set #
theorem
List.set_eq_modifyNth
{α : Type u_1}
(a : α)
(n : Nat)
(l : List α)
:
l.set n a = List.modifyNth (fun (x : α) => a) n l
theorem
List.modifyNth_eq_set_get?
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modifyNth f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l
theorem
List.modifyNth_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
List.modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))
removeNth #
@[deprecated List.length_eraseIdx]
Alias of List.length_eraseIdx
.
tail #
eraseP #
theorem
List.eraseP_cons
{α : Type u_1}
{p : α → Bool}
(a : α)
(l : List α)
:
List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
@[simp]
theorem
List.eraseP_cons_of_pos
{α : Type u_1}
{a : α}
{l : List α}
(p : α → Bool)
(h : p a = true)
:
List.eraseP p (a :: l) = l
@[simp]
theorem
List.eraseP_cons_of_neg
{α : Type u_1}
{a : α}
{l : List α}
(p : α → Bool)
(h : ¬p a = true)
:
List.eraseP p (a :: l) = a :: List.eraseP p l
@[simp]
theorem
List.eraseP_append_left
{α : Type u_1}
{p : α → Bool}
{a : α}
(pa : p a = true)
{l₁ : List α}
(l₂ : List α)
:
a ∈ l₁ → List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
theorem
List.eraseP_append_right
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
(l₂ : List α)
:
(∀ (b : α), b ∈ l₁ → ¬p b = true) → List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂
theorem
List.Sublist.eraseP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁.Sublist l₂ → (List.eraseP p l₁).Sublist (List.eraseP p l₂)
theorem
List.mem_of_mem_eraseP
{α : Type u_1}
{a : α}
{p : α → Bool}
{l : List α}
:
a ∈ List.eraseP p l → a ∈ l
theorem
List.eraseP_map
{β : Type u_1}
{α : Type u_2}
{p : α → Bool}
(f : β → α)
(l : List β)
:
List.eraseP p (List.map f l) = List.map f (List.eraseP (p ∘ f) l)
@[simp]
theorem
List.extractP_eq_find?_eraseP
{α : Type u_1}
{p : α → Bool}
(l : List α)
:
List.extractP p l = (List.find? p l, List.eraseP p l)
theorem
List.extractP_eq_find?_eraseP.go
{α : Type u_1}
{p : α → Bool}
(l : List α)
(acc : Array α)
(xs : List α)
:
l = acc.data ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs)
erase #
theorem
List.erase_eq_eraseP'
{α : Type u_1}
[BEq α]
(a : α)
(l : List α)
:
l.erase a = List.eraseP (fun (x : α) => x == a) l
theorem
List.erase_eq_eraseP
{α : Type u_1}
[BEq α]
[LawfulBEq α]
(a : α)
(l : List α)
:
l.erase a = List.eraseP (fun (x : α) => a == x) l
@[deprecated List.Sublist.erase]
theorem
List.sublist.erase
{α : Type u_1}
[BEq α]
(a : α)
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
(l₁.erase a).Sublist (l₂.erase a)
Alias of List.Sublist.erase
.
filter and partition #
@[simp]
filterMap #
theorem
List.Sublist.filterMap
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
(f : α → Option β)
(s : l₁.Sublist l₂)
:
(List.filterMap f l₁).Sublist (List.filterMap f l₂)
theorem
List.Sublist.filter
{α : Type u_1}
(p : α → Bool)
{l₁ : List α}
{l₂ : List α}
(s : l₁.Sublist l₂)
:
(List.filter p l₁).Sublist (List.filter p l₂)
findIdx #
theorem
List.findIdx_cons
{α : Type u_1}
(p : α → Bool)
(b : α)
(l : List α)
:
List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
theorem
List.findIdx_cons.findIdx_go_succ
{α : Type u_1}
(p : α → Bool)
(l : List α)
(n : Nat)
:
List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
theorem
List.findIdx_of_get?_eq_some
{α : Type u_1}
{p : α → Bool}
{y : α}
{xs : List α}
(w : xs.get? (List.findIdx p xs) = some y)
:
theorem
List.findIdx_get
{α : Type u_1}
{p : α → Bool}
{xs : List α}
{w : List.findIdx p xs < xs.length}
:
p (xs.get ⟨List.findIdx p xs, w⟩) = true
theorem
List.findIdx_get?_eq_get_of_exists
{α : Type u_1}
{p : α → Bool}
{xs : List α}
(h : ∃ (x : α), x ∈ xs ∧ p x = true)
:
xs.get? (List.findIdx p xs) = some (xs.get ⟨List.findIdx p xs, ⋯⟩)
findIdx? #
@[simp]
@[simp]
@[simp]
theorem
List.findIdx?_succ
{α : Type u_1}
{xs : List α}
{p : α → Bool}
{i : Nat}
:
List.findIdx? p xs (i + 1) = Option.map (fun (i : Nat) => i + 1) (List.findIdx? p xs i)
@[simp]
theorem
List.findIdx?_append
{α : Type u_1}
{xs : List α}
{ys : List α}
{p : α → Bool}
:
List.findIdx? p (xs ++ ys) = HOrElse.hOrElse (List.findIdx? p xs) fun (x : Unit) =>
Option.map (fun (i : Nat) => i + xs.length) (List.findIdx? p ys)
@[simp]
theorem
List.findIdx?_replicate
{n : Nat}
:
∀ {α : Type u_1} {a : α} {p : α → Bool},
List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none
pairwise #
theorem
List.Pairwise.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, l₁.Sublist l₂ → List.Pairwise R l₂ → List.Pairwise R l₁
theorem
List.pairwise_map
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → α_1} {R : α_1 → α_1 → Prop} {l : List α},
List.Pairwise R (List.map f l) ↔ List.Pairwise (fun (a b : α) => R (f a) (f b)) l
theorem
List.pairwise_append
{α : Type u_1}
{R : α → α → Prop}
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R l₁ ∧ List.Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b
theorem
List.pairwise_reverse
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
:
List.Pairwise R l.reverse ↔ List.Pairwise (fun (a b : α) => R b a) l
theorem
List.Pairwise.imp
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(H : ∀ {a b : α}, R a b → S a b)
{l : List α}
:
List.Pairwise R l → List.Pairwise S l
replaceF #
theorem
List.replaceF_cons
{α : Type u_1}
{p : α → Option α}
(a : α)
(l : List α)
:
List.replaceF p (a :: l) = match p a with
| none => a :: List.replaceF p l
| some a' => a' :: l
theorem
List.replaceF_cons_of_none
{α : Type u_1}
{a : α}
{l : List α}
(p : α → Option α)
(h : p a = none)
:
List.replaceF p (a :: l) = a :: List.replaceF p l
theorem
List.replaceF_of_forall_none
{α : Type u_1}
{p : α → Option α}
{l : List α}
(h : ∀ (a : α), a ∈ l → p a = none)
:
List.replaceF p l = l
@[simp]
theorem
List.length_replaceF :
∀ {α : Type u_1} {f : α → Option α} {l : List α}, (List.replaceF f l).length = l.length
disjoint #
foldl / foldr #
theorem
List.foldl_hom
{α₁ : Type u_1}
{α₂ : Type u_2}
{β : Type u_3}
(f : α₁ → α₂)
(g₁ : α₁ → β → α₁)
(g₂ : α₂ → β → α₂)
(l : List β)
(init : α₁)
(H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y))
:
List.foldl g₂ (f init) l = f (List.foldl g₁ init l)
theorem
List.foldr_hom
{β₁ : Type u_1}
{β₂ : Type u_2}
{α : Type u_3}
(f : β₁ → β₂)
(g₁ : α → β₁ → β₁)
(g₂ : α → β₂ → β₂)
(l : List α)
(init : β₁)
(H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y))
:
List.foldr g₂ (f init) l = f (List.foldr g₁ init l)
union #
theorem
List.union_def
{α : Type u_1}
[BEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁ ∪ l₂ = List.foldr List.insert l₂ l₁
inter #
theorem
List.inter_def
{α : Type u_1}
[BEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁ ∩ l₂ = List.filter (fun (x : α) => List.elem x l₂) l₁
product #
leftpad #
@[simp]
theorem
List.leftpad_length
{α : Type u_1}
(n : Nat)
(a : α)
(l : List α)
:
(List.leftpad n a l).length = max n l.length
The length of the List returned by List.leftpad n a l
is equal
to the larger of n
and l.length
theorem
List.leftpad_prefix
{α : Type u_1}
(n : Nat)
(a : α)
(l : List α)
:
List.replicate (n - l.length) a <+: List.leftpad n a l
monadic operations #
theorem
List.forIn_eq_bindList
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → β → m (ForInStep β))
(l : List α)
(init : β)
:
forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
diff #
theorem
List.diff_eq_foldl
{α : Type u_1}
[BEq α]
[LawfulBEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁.diff l₂ = List.foldl List.erase l₁ l₂
prefix, suffix, infix #
theorem
List.IsPrefix.filter
{α : Type u_1}
(p : α → Bool)
⦃l₁ : List α⦄
⦃l₂ : List α⦄
(h : l₁ <+: l₂)
:
List.filter p l₁ <+: List.filter p l₂
theorem
List.IsSuffix.filter
{α : Type u_1}
(p : α → Bool)
⦃l₁ : List α⦄
⦃l₂ : List α⦄
(h : l₁ <:+ l₂)
:
List.filter p l₁ <:+ List.filter p l₂
theorem
List.IsInfix.filter
{α : Type u_1}
(p : α → Bool)
⦃l₁ : List α⦄
⦃l₂ : List α⦄
(h : l₁ <:+: l₂)
:
List.filter p l₁ <:+: List.filter p l₂
drop #
Chain #
@[simp]
theorem
List.chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
:
List.Chain R a (b :: l) ↔ R a b ∧ List.Chain R b l
theorem
List.rel_of_chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
(p : List.Chain R a (b :: l))
:
R a b
theorem
List.chain_of_chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
(p : List.Chain R a (b :: l))
:
List.Chain R b l
theorem
List.Chain.imp'
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(HRS : ∀ ⦃a b : α⦄, R a b → S a b)
{a : α}
{b : α}
(Hab : ∀ ⦃c : α⦄, R a c → S b c)
{l : List α}
(p : List.Chain R a l)
:
List.Chain S b l
theorem
List.Chain.imp
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{a : α}
{l : List α}
(p : List.Chain R a l)
:
List.Chain S a l
theorem
List.Pairwise.chain :
∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, List.Pairwise R (a :: l) → List.Chain R a l
range', range #
theorem
List.range'_succ
(s : Nat)
(n : Nat)
(step : Nat)
:
List.range' s (n + 1) step = s :: List.range' (s + step) n step
@[simp]
@[simp]
@[simp]
theorem
List.map_add_range'
(a : Nat)
(s : Nat)
(n : Nat)
(step : Nat)
:
List.map (fun (x : Nat) => a + x) (List.range' s n step) = List.range' (a + s) n step
theorem
List.map_sub_range'
{step : Nat}
(a : Nat)
(s : Nat)
(n : Nat)
(h : a ≤ s)
:
List.map (fun (x : Nat) => x - a) (List.range' s n step) = List.range' (s - a) n step
theorem
List.chain_succ_range'
(s : Nat)
(n : Nat)
(step : Nat)
:
List.Chain (fun (a b : Nat) => b = a + step) s (List.range' (s + step) n step)
theorem
List.chain_lt_range'
(s : Nat)
(n : Nat)
{step : Nat}
(h : 0 < step)
:
List.Chain (fun (x x_1 : Nat) => x < x_1) s (List.range' (s + step) n step)
theorem
List.range'_append
(s : Nat)
(m : Nat)
(n : Nat)
(step : Nat)
:
List.range' s m step ++ List.range' (s + step * m) n step = List.range' s (n + m) step
@[simp]
theorem
List.range'_append_1
(s : Nat)
(m : Nat)
(n : Nat)
:
List.range' s m ++ List.range' (s + m) n = List.range' s (n + m)
theorem
List.range'_sublist_right
{step : Nat}
{s : Nat}
{m : Nat}
{n : Nat}
:
(List.range' s m step).Sublist (List.range' s n step) ↔ m ≤ n
theorem
List.range'_subset_right
{step : Nat}
{s : Nat}
{m : Nat}
{n : Nat}
(step0 : 0 < step)
:
List.range' s m step ⊆ List.range' s n step ↔ m ≤ n
theorem
List.range'_subset_right_1
{s : Nat}
{m : Nat}
{n : Nat}
:
List.range' s m ⊆ List.range' s n ↔ m ≤ n
@[simp]
theorem
List.getElem_range'
{n : Nat}
{m : Nat}
{step : Nat}
(i : Nat)
(H : i < (List.range' n m step).length)
:
(List.range' n m step)[i] = n + step * i
@[deprecated List.getElem_range']
theorem
List.get_range'
{n : Nat}
{m : Nat}
{step : Nat}
(i : Nat)
(H : i < (List.range' n m step).length)
:
(List.range' n m step).get ⟨i, H⟩ = n + step * i
theorem
List.range'_concat
{step : Nat}
(s : Nat)
(n : Nat)
:
List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
theorem
List.range'_1_concat
(s : Nat)
(n : Nat)
:
List.range' s (n + 1) = List.range' s n ++ [s + n]
theorem
List.range_loop_range'
(s : Nat)
(n : Nat)
:
List.range.loop s (List.range' s n) = List.range' 0 (n + s)
theorem
List.range_succ_eq_map
(n : Nat)
:
List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
theorem
List.range'_eq_map_range
(s : Nat)
(n : Nat)
:
List.range' s n = List.map (fun (x : Nat) => s + x) (List.range n)
@[simp]
@[simp]
theorem
List.getElem_range
{n : Nat}
(m : Nat)
(h : m < (List.range n).length)
:
(List.range n)[m] = m
@[deprecated List.getElem?_range]
@[deprecated List.getElem_range]
theorem
List.get_range
{n : Nat}
(i : Nat)
(H : i < (List.range n).length)
:
(List.range n).get ⟨i, H⟩ = i
theorem
List.range_add
(a : Nat)
(b : Nat)
:
List.range (a + b) = List.range a ++ List.map (fun (x : Nat) => a + x) (List.range b)
theorem
List.reverse_range'
(s : Nat)
(n : Nat)
:
(List.range' s n).reverse = List.map (fun (x : Nat) => s + n - 1 - x) (List.range n)
enum, enumFrom #
@[simp]
theorem
List.enumFrom_map_fst
{α : Type u_1}
(n : Nat)
(l : List α)
:
List.map Prod.fst (List.enumFrom n l) = List.range' n l.length
@[simp]
theorem
List.enum_map_fst
{α : Type u_1}
(l : List α)
:
List.map Prod.fst l.enum = List.range l.length
indexOf and indexesOf #
theorem
List.foldrIdx_start
{α : Type u_1}
{xs : List α}
:
∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat},
List.foldrIdx f i xs s = List.foldrIdx (fun (i : Nat) => f (i + s)) i xs
@[simp]
theorem
List.foldrIdx_cons
{α : Type u_1}
{x : α}
{xs : List α}
:
∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat},
List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
theorem
List.findIdxs_cons
{α : Type u_1}
{x : α}
{xs : List α}
{p : α → Bool}
:
List.findIdxs p (x :: xs) = bif p x then 0 :: List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
else List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
theorem
List.indexesOf_cons
{α : Type u_1}
{x : α}
{xs : List α}
{y : α}
[BEq α]
:
List.indexesOf y (x :: xs) = bif x == y then 0 :: List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
else List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
theorem
List.indexOf_cons
{α : Type u_1}
{x : α}
{xs : List α}
{y : α}
[BEq α]
:
List.indexOf y (x :: xs) = bif x == y then 0 else List.indexOf y xs + 1
theorem
List.indexOf_mem_indexesOf
{α : Type u_1}
{x : α}
[BEq α]
[LawfulBEq α]
{xs : List α}
(m : x ∈ xs)
:
List.indexOf x xs ∈ List.indexesOf x xs
theorem
List.merge_loop_nil_left
{α : Type u_1}
(s : α → α → Bool)
(r : List α)
(t : List α)
:
List.merge.loop s [] r t = t.reverseAux r
theorem
List.merge_loop_nil_right
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(t : List α)
:
List.merge.loop s l [] t = t.reverseAux l
theorem
List.merge_loop
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(r : List α)
(t : List α)
:
List.merge.loop s l r t = t.reverseAux (List.merge s l r)
@[simp]
@[simp]
theorem
List.cons_merge_cons
{α : Type u_1}
(s : α → α → Bool)
(a : α)
(b : α)
(l : List α)
(r : List α)
:
List.merge s (a :: l) (b :: r) = if s a b = true then a :: List.merge s l (b :: r) else b :: List.merge s (a :: l) r
@[simp]
theorem
List.cons_merge_cons_pos
{α : Type u_1}
{a : α}
{b : α}
(s : α → α → Bool)
(l : List α)
(r : List α)
(h : s a b = true)
:
List.merge s (a :: l) (b :: r) = a :: List.merge s l (b :: r)
@[simp, irreducible]
theorem
List.length_merge
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(r : List α)
:
(List.merge s l r).length = l.length + r.length
theorem
List.mem_merge_left
{α : Type u_1}
{x : α}
{l : List α}
{r : List α}
(s : α → α → Bool)
(h : x ∈ l)
:
x ∈ List.merge s l r
theorem
List.mem_merge_right
{α : Type u_1}
{x : α}
{r : List α}
{l : List α}
(s : α → α → Bool)
(h : x ∈ r)
:
x ∈ List.merge s l r