Some lemmas about lists involving sets

Split out from Data.List.Basic to reduce its dependencies.

ink

theorem List.range_map {α : Type u_2} {β : Type u_1} (f : α → β) : Set.range (List.map f) = { l | ∀ (x : β), x ∈ l → x ∈ Set.range f }

ink

theorem List.range_map_coe {α : Type u_1} (s : Set α) : Set.range (List.map Subtype.val) = { l | ∀ (x : α), x ∈ l → x ∈ s }

ink

instance List.canLift {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [inst : CanLift α β c p] : CanLift (List α) (List β) (List.map c) fun l => (x : α) → x ∈ l → p x

If each element of a list can be lifted to some type, then the whole list can be lifted to this type.

Equations

• List.canLift c p = { prf := (_ : ∀ (l : List α), ((x : α) → x ∈ l → p x) → ∃ y, List.map c y = l) }

ink

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 }

ink

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)

ink

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)

ink

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)

ink

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)