Some lemmas about lists involving sets #
Split out from Data.List.Basic
to reduce its dependencies.
@[deprecated List.tail_reverse (since := "2024-12-10")]
Alias of List.tail_reverse
.
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 : α)
:
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 : α)
:
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 : α)
:
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 : α)
:
MapAccumr and Foldr #
Some lemmas relation mapAccumr
and foldr