Some lemmas about lists involving sets #
Split out from Data.List.Basic
to reduce its dependencies.
theorem
List.countP_flatMap
{α : Type u_1}
{β : Type u_2}
(p : β → Bool)
(l : List α)
(f : α → List β)
:
List.countP p (l.flatMap f) = (List.map (List.countP p ∘ f) l).sum
theorem
List.count_flatMap
{α : Type u_1}
{β : Type u_2}
[BEq β]
(l : List α)
(f : α → List β)
(x : β)
:
List.count x (l.flatMap f) = (List.map (List.count x ∘ f) l).sum
@[deprecated List.getElem_reverse]
Alias of List.getElem_reverse
.
@[deprecated List.tail_reverse]
theorem
List.tail_reverse_eq_reverse_dropLast
{α : Type u_1}
(l : List α)
:
l.reverse.tail = l.dropLast.reverse
Alias of List.tail_reverse
.
@[deprecated List.getElem_tail]
Alias of List.getElem_tail
.
theorem
List.injOn_insertIdx_index_of_not_mem
{α : Type u_1}
(l : List α)
(x : α)
(hx : x ∉ l)
:
Set.InjOn (fun (k : ℕ) => List.insertIdx k x l) {n : ℕ | n ≤ l.length}
@[deprecated List.injOn_insertIdx_index_of_not_mem]
theorem
List.injOn_insertNth_index_of_not_mem
{α : Type u_1}
(l : List α)
(x : α)
(hx : x ∉ l)
:
Set.InjOn (fun (k : ℕ) => List.insertIdx k x l) {n : ℕ | n ≤ l.length}
Alias of List.injOn_insertIdx_index_of_not_mem
.
theorem
List.foldr_range_subset_of_range_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → α → α}
{g : γ → α → α}
(hfg : Set.range f ⊆ Set.range g)
(a : α)
:
Set.range (List.foldr f a) ⊆ Set.range (List.foldr g a)
theorem
List.foldl_range_subset_of_range_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → α}
{g : α → γ → α}
(hfg : (Set.range fun (a : β) (c : α) => f c a) ⊆ Set.range fun (b : γ) (c : α) => g c b)
(a : α)
:
Set.range (List.foldl f a) ⊆ Set.range (List.foldl g a)
theorem
List.foldr_range_eq_of_range_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → α → α}
{g : γ → α → α}
(hfg : Set.range f = Set.range g)
(a : α)
:
Set.range (List.foldr f a) = Set.range (List.foldr g a)
theorem
List.foldl_range_eq_of_range_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → α}
{g : α → γ → α}
(hfg : (Set.range fun (a : β) (c : α) => f c a) = Set.range fun (b : γ) (c : α) => g c b)
(a : α)
:
Set.range (List.foldl f a) = Set.range (List.foldl g a)
MapAccumr and Foldr #
Some lemmas relation mapAccumr
and foldr
theorem
List.mapAccumr_eq_foldr
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
(f : α → σ → σ × β)
(as : List α)
(s : σ)
:
List.mapAccumr f as s = List.foldr
(fun (a : α) (s : σ × List β) =>
let r := f a s.1;
(r.1, r.2 :: s.2))
(s, []) as
theorem
List.mapAccumr₂_eq_foldr
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
{φ : Type u_5}
(f : α → β → σ → σ × φ)
(as : List α)
(bs : List β)
(s : σ)
:
List.mapAccumr₂ f as bs s = List.foldr
(fun (ab : α × β) (s : σ × List φ) =>
let r := f ab.1 ab.2 s.1;
(r.1, r.2 :: s.2))
(s, []) (as.zip bs)