Some lemmas about lists involving sets #
Split out from Data.List.Basic
to reduce its dependencies.
instance
List.canLift
{α : Type u_1}
{β : Type u_2}
(c : β → α)
(p : α → Prop)
[inst : CanLift α β c p]
:
If each element of a list can be lifted to some type, then the whole list can be lifted to this type.
theorem
List.injOn_insertNth_index_of_not_mem
{α : Type u_1}
(l : List α)
(x : α)
(hx : ¬x ∈ l)
:
Set.InjOn (fun k => List.insertNth k x l) { n | n ≤ List.length l }
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)