zip & unzip #
This file provides results about List.zipWith, List.zip and List.unzip (definitions are in
core Lean).
zipWith f l₁ l₂ applies f : α → β → γ pointwise to a list l₁ : List α and l₂ : List β. It
applies, until one of the lists is exhausted. For example,
zipWith f [0, 1, 2] [6.28, 31] = [f 0 6.28, f 1 31].
zip is zipWith applied to Prod.mk. For example,
zip [a₁, a₂] [b₁, b₂, b₃] = [(a₁, b₁), (a₂, b₂)].
unzip undoes zip. For example, unzip [(a₁, b₁), (a₂, b₂)] = ([a₁, a₂], [b₁, b₂]).
theorem
List.forall_zipWith
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{f : α → β → γ}
{p : γ → Prop}
{l₁ : List α}
{l₂ : List β}
:
l₁.length = l₂.length → (List.Forall p (List.zipWith f l₁ l₂) ↔ List.Forall₂ (fun (x : α) (y : β) => p (f x y)) l₁ l₂)
theorem
List.zipWith_congr
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f g : α → β → γ)
(la : List α)
(lb : List β)
(h : List.Forall₂ (fun (a : α) (b : β) => f a b = g a b) la lb)
:
List.zipWith f la lb = List.zipWith g la lb
theorem
List.zipWith_zipWith_left
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
{ε : Type u_4}
(f : δ → γ → ε)
(g : α → β → δ)
(la : List α)
(lb : List β)
(lc : List γ)
:
List.zipWith f (List.zipWith g la lb) lc = List.zipWith3 (fun (a : α) (b : β) (c : γ) => f (g a b) c) la lb lc
theorem
List.zipWith_zipWith_right
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
{ε : Type u_4}
(f : α → δ → ε)
(g : β → γ → δ)
(la : List α)
(lb : List β)
(lc : List γ)
:
List.zipWith f la (List.zipWith g lb lc) = List.zipWith3 (fun (a : α) (b : β) (c : γ) => f a (g b c)) la lb lc
@[simp]
theorem
List.zipWith3_same_left
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → α → β → γ)
(la : List α)
(lb : List β)
:
List.zipWith3 f la la lb = List.zipWith (fun (a : α) (b : β) => f a a b) la lb
@[simp]
theorem
List.zipWith3_same_mid
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → α → γ)
(la : List α)
(lb : List β)
:
List.zipWith3 f la lb la = List.zipWith (fun (a : α) (b : β) => f a b a) la lb
@[simp]
theorem
List.zipWith3_same_right
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → β → γ)
(la : List α)
(lb : List β)
:
List.zipWith3 f la lb lb = List.zipWith (fun (a : α) (b : β) => f a b b) la lb
theorem
List.instIsSymmOpZipWith
{α : Type u}
{β : Type u_1}
(f : α → α → β)
[IsSymmOp f]
:
IsSymmOp (List.zipWith f)
@[deprecated List.getElem?_zipWith']
theorem
List.getElem?_zip_with
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{l₁ : List α}
{l₂ : List β}
{f : α → β → γ}
{i : ℕ}
:
(List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun (g : β → γ) => Option.map g l₂[i]?
Alias of List.getElem?_zipWith'.
Variant of getElem?_zipWith using Option.map and Option.bind rather than a match.
theorem
List.get?_zipWith'
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → γ)
(l₁ : List α)
(l₂ : List β)
(i : ℕ)
:
(List.zipWith f l₁ l₂).get? i = (Option.map f (l₁.get? i)).bind fun (g : β → γ) => Option.map g (l₂.get? i)
@[deprecated List.get?_zipWith']
theorem
List.get?_zip_with
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → γ)
(l₁ : List α)
(l₂ : List β)
(i : ℕ)
:
(List.zipWith f l₁ l₂).get? i = (Option.map f (l₁.get? i)).bind fun (g : β → γ) => Option.map g (l₂.get? i)
Alias of List.get?_zipWith'.
@[deprecated List.getElem?_zipWith_eq_some]
theorem
List.getElem?_zip_with_eq_some
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{l₁ : List α}
{l₂ : List β}
{z : γ}
{i : ℕ}
:
Alias of List.getElem?_zipWith_eq_some.
@[deprecated List.get?_zipWith_eq_some]
theorem
List.get?_zip_with_eq_some
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
(f : α → β → γ)
(l₁ : List α)
(l₂ : List β)
(z : γ)
(i : ℕ)
:
Alias of List.get?_zipWith_eq_some.
@[deprecated List.getElem_zipWith]
theorem
List.get_zipWith
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{f : α → β → γ}
{l : List α}
{l' : List β}
{i : Fin (List.zipWith f l l').length}
:
(List.zipWith f l l').get i = f (l.get ⟨↑i, ⋯⟩) (l'.get ⟨↑i, ⋯⟩)