Length and indexing of concatenated pairs

Flattening a list of two-element blocks doubles its length and places the two components at the even and odd positions.

theorem RS.len_flatMap_pair {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) : (List.flatMap (fun (x : α) => [f x, g x]) L).length = 2 * L.length

A list of pairs has twice as many entries as its source.

theorem RS.getElemOption_flatMap_pair_even {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j]? = Option.map f L[j]?

Even positions in a list of pairs come from the first component.

theorem RS.getElemOption_flatMap_pair_odd {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j + 1]? = Option.map g L[j]?

Odd positions in a list of pairs come from the second component.

theorem RS.getElemOption_self_paired {α : Type u_1} (L : List α) (h : α → α) (j : ℕ) : (List.flatMap (fun (x : α) => [x, h x]) L)[2 * j + 1]? = Option.map h (List.flatMap (fun (x : α) => [x, h x]) L)[2 * j]?

In a flatMap of [x, h x] blocks, element 2j+1 is h applied to element 2j.

theorem RS.getElem_flatMap_pair_even {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) (hj : j < L.length) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j] = f L[j]

The entry at an even position is the first component.

theorem RS.getElem_flatMap_pair_odd {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) (hj : j < L.length) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j + 1] = g L[j]

The entry at an odd position is the second component.

theorem RS.getElem?_flatMap_pair_even {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j]? = Option.map f L[j]?

Alias of RS.getElemOption_flatMap_pair_even.

---

Even positions in a list of pairs come from the first component.

theorem RS.getElem?_flatMap_pair_odd {α : Type u_1} {β : Type u_2} (L : List α) (f g : α → β) (j : ℕ) : (List.flatMap (fun (x : α) => [f x, g x]) L)[2 * j + 1]? = Option.map g L[j]?

Alias of RS.getElemOption_flatMap_pair_odd.

---

Odd positions in a list of pairs come from the second component.

theorem RS.getElem?_self_paired {α : Type u_1} (L : List α) (h : α → α) (j : ℕ) : (List.flatMap (fun (x : α) => [x, h x]) L)[2 * j + 1]? = Option.map h (List.flatMap (fun (x : α) => [x, h x]) L)[2 * j]?

Alias of RS.getElemOption_self_paired.

---

In a flatMap of [x, h x] blocks, element 2j+1 is h applied to element 2j.